diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-04-23 14:49:12 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-04-23 14:49:12 +0200 |
| commit | 3ca2af08f068eb1edf638b8ef602b816823873e0 (patch) | |
| tree | 92c1020c81a62c972a1e5c291cf4c3fa65792df0 /lib/Camlcoq.ml | |
| parent | 8c2e9c25bab0118a71fe27bbe539ac6464effde2 (diff) | |
| download | compcert-kvx-3ca2af08f068eb1edf638b8ef602b816823873e0.tar.gz compcert-kvx-3ca2af08f068eb1edf638b8ef602b816823873e0.zip | |
Give a name to the type of atoms.
Diffstat (limited to 'lib/Camlcoq.ml')
| -rw-r--r-- | lib/Camlcoq.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml index dd896367..68c095f0 100644 --- a/lib/Camlcoq.ml +++ b/lib/Camlcoq.ml @@ -281,8 +281,10 @@ let coqint_of_camlint64 : int64 -> Integers.Int64.int = Z.of_uint64 (* Atoms (positive integers representing strings) *) -let atom_of_string = (Hashtbl.create 17 : (string, positive) Hashtbl.t) -let string_of_atom = (Hashtbl.create 17 : (positive, string) Hashtbl.t) +type atom = positive + +let atom_of_string = (Hashtbl.create 17 : (string, atom) Hashtbl.t) +let string_of_atom = (Hashtbl.create 17 : (atom, string) Hashtbl.t) let next_atom = ref Coq_xH let intern_string s = |