Huge reorganization of matita and ocaml.

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

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index 4b4e0fed9f89f529d1e79f6036572dbc1e2b1874..6e200cc310e1559db1e3b1875f6d44a7332294c6 100644 (file)
--- a/helm/ocaml/cic/cic.ml
+++ b/helm/ocaml/cic/cic.ml
@@ -216,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