- removed some unneeded dependencies from debian/control

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

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index fd46c22b4820e74232d3e18e2e8a2eb46b073041..cb2af219b89daaa904577ff83c93ebb8e1c98086 100644 (file)
--- a/helm/ocaml/cic/cic.ml
+++ b/helm/ocaml/cic/cic.ml
@@ -51,6 +51,7 @@ and sort =
    Prop
  | Set
  | Type
+ | CProp
 and name =
    Name of string
  | Anonymous
@@ -171,7 +172,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 +186,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
+;;