aboutsummaryrefslogtreecommitdiff
path: root/kernel/csymtable.ml
diff options
context:
space:
mode:
authorGaëtan Gilbert2018-06-23 15:38:00 +0200
committerGaëtan Gilbert2018-07-24 13:49:17 +0200
commit0108db19c96e1b46346f032964f2cca3f8149cb3 (patch)
tree6414910c08328fceeb45c82414bea1ee0b601c91 /kernel/csymtable.ml
parent7817af48a554573fb649028263ecfc0fabe400d8 (diff)
Projections use index representation
The upper layers still need a mapping constant -> projection, which is provided by Recordops.
Diffstat (limited to 'kernel/csymtable.ml')
-rw-r--r--kernel/csymtable.ml6
1 files changed, 1 insertions, 5 deletions
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index bbe0937820..bb9231d000 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -77,11 +77,7 @@ module AnnotTable = Hashtbl.Make (struct
let hash = hash_annot_switch
end)
-module ProjNameTable = Hashtbl.Make (struct
- type t = Constant.t
- let equal = Constant.equal
- let hash = Constant.hash
-end)
+module ProjNameTable = Hashtbl.Make (Projection.Repr)
let str_cst_tbl : int SConstTable.t = SConstTable.create 31