X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2Fcic.ml;h=f9e99260d52944640d65ace9d5d9b6909be8cd42;hb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;hp=cb2af219b89daaa904577ff83c93ebb8e1c98086;hpb=296b163c8a2b09a6f87cbab15c2016de92fc8e70;p=helm.git diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml index cb2af219b..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,7 @@ type anntarget = and sort = Prop | Set - | Type + | Type of CicUniv.universe | CProp and name = Name of string @@ -62,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 *) @@ -82,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 *) @@ -123,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 *)