X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic%2Fcic.ml;h=6d58e6164336dbb8fecf6a5e8007f5ef77b31bae;hb=d1010e05c0d73e3b44d3d971592bd8be9e1e0752;hp=fd46c22b4820e74232d3e18e2e8a2eb46b073041;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index fd46c22b4..6d58e6164 100644
--- 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
+;;