diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-16 19:43:35 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-16 19:43:35 +0200 |
| commit | 98cddc7ba45b34fbd71d9a80c27a8e5ec6b311b0 (patch) | |
| tree | 5a39f62c4e1526dd9e047f74efca164c59504f95 /lib/Camlcoq.ml | |
| parent | 3344bcf59acb1ae8d43a0d15acb4b824689e706d (diff) | |
| download | compcert-kvx-98cddc7ba45b34fbd71d9a80c27a8e5ec6b311b0.tar.gz compcert-kvx-98cddc7ba45b34fbd71d9a80c27a8e5ec6b311b0.zip | |
Move more functionality in the new interface.
Added functions to add more information to the debuging interface,
like the struct layout with offsets, bitifiled layout and removed
the no longer needed mapping from stamp to atom.
Diffstat (limited to 'lib/Camlcoq.ml')
| -rw-r--r-- | lib/Camlcoq.ml | 10 |
1 files changed, 1 insertions, 9 deletions
diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml index 5eb52e88..c50b3230 100644 --- a/lib/Camlcoq.ml +++ b/lib/Camlcoq.ml @@ -284,7 +284,6 @@ let coqint_of_camlint64 : int64 -> Integers.Int64.int = Z.of_uint64 type atom = positive let atom_of_string = (Hashtbl.create 17 : (string, atom) Hashtbl.t) -let atom_of_stamp = (Hashtbl.create 17: (int, atom) Hashtbl.t) let string_of_atom = (Hashtbl.create 17 : (atom, string) Hashtbl.t) let next_atom = ref Coq_xH @@ -296,14 +295,7 @@ let intern_string s = next_atom := Pos.succ !next_atom; Hashtbl.add atom_of_string s a; Hashtbl.add string_of_atom a s; - a - -let add_stamp s a = - Hashtbl.add atom_of_stamp s a - -let stamp_atom s = - Hashtbl.find atom_of_stamp s - + a let extern_atom a = try Hashtbl.find string_of_atom a |