X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2Fcic.ml;h=4b4e0fed9f89f529d1e79f6036572dbc1e2b1874;hb=99b249b23524cda2d91602ee088fef1a7be253ee;hp=aacaabda95490e4f9e1cfc9df946f6be70e08c8c;hpb=33c27a9941fb0ba8be59e041140aa873b4c4d700;p=helm.git

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index aacaabda9..4b4e0fed9 100644
--- a/helm/ocaml/cic/cic.ml
+++ b/helm/ocaml/cic/cic.ml
@@ -66,8 +66,9 @@ type object_class =
   [ `Coercion
   | `Elim of sort   (** elimination principle; if sort is Type, the universe is
                       * not relevant *)
-  | `Record of string list (** inductive type that encodes a record;
-                               the arguments are the record fields *)
+  | `Record of (string * bool) list (** 
+                        inductive type that encodes a record; the arguments are
+                        the record fields names and if they are coercions *)
   | `Projection     (** record projection *)
   ]
 
@@ -222,3 +223,12 @@ type anntarget =
  | Conjecture of annconjecture
  | Hypothesis of annhypothesis
 
+module CicHash =
+ Hashtbl.Make
+  (struct
+    type t = term
+    let equal = (==)
+    let hash = Hashtbl.hash
+   end)
+;;
+