type anntarget =
Object of annobj
| Term of annterm
+ | Conjecture of annconjecture
+ | Hypothesis of annhypothesis
(* INTERNAL REPRESENTATION OF CIC OBJECTS AND TERMS *)
and sort =
| LetIn of name * term * term (* binder, term, target *)
| Appl of term list (* arguments *)
| Const of UriManager.uri * int (* uri, number of cookings*)
- | Abst of UriManager.uri (* uri *)
| MutInd of UriManager.uri * int * int (* uri, cookingsno, typeno*)
+ (* typeno is 0 based *)
| MutConstruct of UriManager.uri * int * (* uri, cookingsno, *)
int * int (* typeno, consno *)
+ (* consno is 1 based *)
(*CSC: serve cookingsno?*)
| MutCase of UriManager.uri * int * (* ind. uri, cookingsno, *)
int * (* ind. typeno, *)
and coInductiveFun =
string * term * term (* name, type, body *)
-and metasenv = (int * context * term) list (* a metasenv is a list of declarations of metas *)
+(* a metasenv is a list of declarations of metas *)
+and conjecture = int * context * term
+and metasenv = conjecture list
-and annmetasenv = (int * anncontext * annterm) list (* a metasenv is a list of declarations of metas *)
+(* a metasenv is a list of declarations of metas *)
+and annconjecture = id * int * anncontext * annterm
+and annmetasenv = annconjecture list
and annterm =
ARel of id * int * string (* DeBrujin index, binder *)
| ALetIn of id * name * annterm * annterm (* binder, term, target *)
| AAppl of id * annterm list (* arguments *)
| AConst of id * UriManager.uri * int (* uri, number of cookings*)
- | AAbst of id * UriManager.uri (* uri *)
| AMutInd of id * UriManager.uri * int * int (* uri, cookingsno, typeno*)
+ (* typeno is 0 based *)
| AMutConstruct of id * UriManager.uri * int * (* uri, cookingsno, *)
int * int (* typeno, consno *)
+ (* consno is 1 based *)
(*CSC: serve cookingsno?*)
| AMutCase of id * UriManager.uri * int * (* ind. uri, cookingsno *)
int * (* ind. typeno, *)
Possible of 'a (* an approximation to something *)
| Actual of 'a (* something *)
-and context_entry = (* Contexts are lists of context_entry *)
+and context_entry = (* A declaration or definition *)
Decl of term
| Def of term
-and context = ((name * context_entry) option) list
+and hypothesis =
+ (name * context_entry) option (* None means no more accessible *)
-and anncontext_entry = (* Contexts are lists of context_entry *)
+and context = hypothesis list
+
+and anncontext_entry = (* A declaration or definition *)
ADecl of annterm
| ADef of annterm
-and anncontext = ((name * anncontext_entry) option) list;;
+and annhypothesis =
+ id * (name * anncontext_entry) option (* None means no more accessible *)
+
+and anncontext = annhypothesis list;;