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

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index fd46c22b4..f9e99260d 100644
--- a/helm/ocaml/cic/cic.ml
+++ b/helm/ocaml/cic/cic.ml
@@ -39,6 +39,8 @@
 type id = string  (* the abstract type of the (annotated) node identifiers *)
 type 'term explicit_named_substitution = (UriManager.uri * 'term) list
 
+type implicit_annotation = [ `Closed | `Type ]
+
 type anntarget =
    Object of annobj         (* if annobj is a Constant, this is its type *)
  | ConstantBody of annobj
@@ -50,7 +52,8 @@ type anntarget =
 and sort =
    Prop
  | Set
- | Type
+ | Type of CicUniv.universe
+ | CProp
 and name =
    Name of string
  | Anonymous
@@ -61,7 +64,7 @@ and term =
  | Meta of int * (term option) list                 (* numeric id,    *)
                                                     (*  local context *)
  | Sort of sort                                     (* sort *)
- | Implicit                                         (* *)
+ | Implicit of implicit_annotation option           (* *)
  | Cast of term * term                              (* value, type *)
  | Prod of name * term * term                       (* binder, source, target *)
  | Lambda of name * term * term                     (* binder, source, target *)
@@ -81,8 +84,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              *)
@@ -122,7 +125,7 @@ and annterm =
  | AMeta of id * int * (annterm option) list        (* numeric id,    *)
                                                     (*  local context *)
  | ASort of id * sort                               (* sort *)
- | AImplicit of id                                  (* *)
+ | AImplicit of id * implicit_annotation option     (* *)
  | ACast of id * annterm * annterm                  (* value, type *)
  | AProd of id * name * annterm * annterm           (* binder, source, target *)
  | ALambda of id * name * annterm * annterm         (* binder, source, target *)
@@ -171,7 +174,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 +188,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
+;;