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 6d58e6164336dbb8fecf6a5e8007f5ef77b31bae..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              *)