X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2Fcic.ml;h=6e200cc310e1559db1e3b1875f6d44a7332294c6;hb=1a40d93d10be4ee71ae9474384af931d70918690;hp=624a3021640ea23eb3b961a06578dbf72ed4d539;hpb=86241d46558e3a4979fc786e47ce78f90eb9190c;p=helm.git

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index 624a30216..6e200cc31 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 *)
   ]
 
@@ -215,6 +216,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