X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2Fcic.ml;h=64825e505dbc717585e0b444cd19e97d1c3762a9;hb=ab72cb44a09c93e1d540f7ac9bc7eae2f4d09f2f;hp=4b4e0fed9f89f529d1e79f6036572dbc1e2b1874;hpb=cf3635c0830661f59d16339cd7fc9c3b948fcbc8;p=helm.git

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index 4b4e0fed9..64825e505 100644
--- 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
@@ -216,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