ZACK: export a top level function for parsing terms, it can't be bypassed due to...

[helm.git] / components / cic / cic.ml

diff --git a/components/cic/cic.ml b/components/cic/cic.ml
index 64825e505dbc717585e0b444cd19e97d1c3762a9..20a6cb457dec63c700283ac952204357c38ab0de 100644 (file)
--- a/components/cic/cic.ml
+++ b/components/cic/cic.ml
@@ -62,6 +62,7 @@ type object_flavour =
   | `Remark
   | `Theorem
   | `Variant
+  | `Axiom
   ]
 
 type object_class =
@@ -234,7 +235,7 @@ module CicHash =
   (struct
     type t = term
     let equal = (==)
-    let hash = Hashtbl.hash
+    let hash = Hashtbl.hash_param 100 1000 
    end)
 ;;