added contextual menu to act over selected terms

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

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index aacaabda95490e4f9e1cfc9df946f6be70e08c8c..4b4e0fed9f89f529d1e79f6036572dbc1e2b1874 100644 (file)
--- 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)
+;;
+