Defs in context may now have an optional type (when unknown).

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

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index fd46c22b4820e74232d3e18e2e8a2eb46b073041..6d58e6164336dbb8fecf6a5e8007f5ef77b31bae 100644 (file)
--- a/helm/ocaml/cic/cic.ml
+++ b/helm/ocaml/cic/cic.ml
@@ -171,7 +171,7 @@ and annotation =
 
 and context_entry =                            (* A declaration or definition *)
    Decl of term
- | Def of term
+ | Def of term * term option                   (* body, type (if known) *)
 
 and hypothesis =
  (name * context_entry) option               (* None means no more accessible *)
@@ -185,4 +185,5 @@ and anncontext_entry =                         (* A declaration or definition *)
 and annhypothesis =
  id * (name * anncontext_entry) option       (* None means no more accessible *)
 
-and anncontext = annhypothesis list;;
+and anncontext = annhypothesis list
+;;