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
Prop
| Set
| Type
+ | CProp
and name =
Name of string
| Anonymous
| 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 *)
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 *)
| 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 *)