| LetIn of name * term * term (* binder, term, target *)
| Appl of term list (* arguments *)
| Const of UriManager.uri * int (* uri, number of cookings*)
| LetIn of name * term * term (* binder, term, target *)
| Appl of term list (* arguments *)
| Const of UriManager.uri * int (* uri, number of cookings*)
| MutConstruct of UriManager.uri * int * (* uri, cookingsno, *)
int * int (* typeno, consno *)
| MutConstruct of UriManager.uri * int * (* uri, cookingsno, *)
int * int (* typeno, consno *)
(*CSC: serve cookingsno?*)
| MutCase of UriManager.uri * int * (* ind. uri, cookingsno, *)
int * (* ind. typeno, *)
(*CSC: serve cookingsno?*)
| MutCase of UriManager.uri * int * (* ind. uri, cookingsno, *)
int * (* ind. typeno, *)
-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
| 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*)
| 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*)
| AMutConstruct of id * UriManager.uri * int * (* uri, cookingsno, *)
int * int (* typeno, consno *)
| AMutConstruct of id * UriManager.uri * int * (* uri, cookingsno, *)
int * int (* typeno, consno *)
(*CSC: serve cookingsno?*)
| AMutCase of id * UriManager.uri * int * (* ind. uri, cookingsno *)
int * (* ind. typeno, *)
(*CSC: serve cookingsno?*)
| AMutCase of id * UriManager.uri * int * (* ind. uri, cookingsno *)
int * (* ind. typeno, *)