added (placeholder) distribution stuff for matita

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

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index aacaabda95490e4f9e1cfc9df946f6be70e08c8c..64825e505dbc717585e0b444cd19e97d1c3762a9 100644 (file)
--- a/helm/ocaml/cic/cic.ml
+++ b/helm/ocaml/cic/cic.ml
@@ -35,6 +35,8 @@
 (*                                                                           *)
 (*****************************************************************************)
 
+(* $Id$ *)
+
 (* STUFF TO MANAGE IDENTIFIERS *)
 type id = string  (* the abstract type of the (annotated) node identifiers *)
 type 'term explicit_named_substitution = (UriManager.uri * 'term) list
@@ -66,8 +68,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 *)
   ]
 
@@ -215,6 +218,10 @@ and annhypothesis =
 and anncontext = annhypothesis list
 ;;
 
+type lazy_term =
+ context -> metasenv -> CicUniv.universe_graph ->
+  term * metasenv * CicUniv.universe_graph
+
 type anntarget =
    Object of annobj         (* if annobj is a Constant, this is its type *)
  | ConstantBody of annobj
@@ -222,3 +229,12 @@ type anntarget =
  | Conjecture of annconjecture
  | Hypothesis of annhypothesis
 
+module CicHash =
+ Hashtbl.Make
+  (struct
+    type t = term
+    let equal = (==)
+    let hash = Hashtbl.hash
+   end)
+;;
+