added testlibrary script

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

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index fd46c22b4820e74232d3e18e2e8a2eb46b073041..46126ff319236800f1a800ad255e2338a9bc24ef 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
@@ -81,8 +82,8 @@ and term =
     int *                                           (*  ind. typeno,         *)
     term * term *                                   (*  outtype, ind. term   *)
     term list                                       (*  patterns             *)
- | Fix of int * inductiveFun list                   (* funno, functions *)
- | CoFix of int * coInductiveFun list               (* funno, functions *)
+ | Fix of int * inductiveFun list                   (* funno (0 based), funs *)
+ | CoFix of int * coInductiveFun list               (* funno (0 based), funs *)
 and obj =
    Constant of string * term option * term *      (* id, body, type,          *)
     UriManager.uri list                           (*  parameters              *)
@@ -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
+;;