minimal changes:

[helm.git] / helm / ocaml / cic / cic.ml

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index b2f6dd8f1c87985d8bf3672e78595067c6cf319f..fd46c22b4820e74232d3e18e2e8a2eb46b073041 100644 (file)
--- a/helm/ocaml/cic/cic.ml
+++ b/helm/ocaml/cic/cic.ml
@@ -102,11 +102,15 @@ and inductiveFun =
 and coInductiveFun =
  string * term * term                         (* name, type, body *)
 
-(* a metasenv is a list of declarations of metas *)
+(* a metasenv is a list of declarations of metas in declarations *)
+(* order (i.e. [oldest ; ... ; newest]). Older variables can not *)
+(* depend on new ones.                                           *)
 and conjecture = int * context * term
 and metasenv = conjecture list
 
-(* a metasenv is a list of declarations of metas *)
+(* a metasenv is a list of declarations of metas in declarations *)
+(* order (i.e. [oldest ; ... ; newest]). Older variables can not *)
+(* depend on new ones.                                           *)
 and annconjecture = id * int * anncontext * annterm
 and annmetasenv = annconjecture list
 
@@ -154,7 +158,7 @@ and annobj =
     anninductiveType list *                         (* inductive types ,      *)
     UriManager.uri list * int                       (*  parameters,n ind. pars*)
 and anninductiveType = 
- string * bool * annterm *                    (* typename, inductive, arity *)
+ id * string * bool * annterm *               (* typename, inductive, arity *)
   annconstructor list                         (*  constructors              *)
 and annconstructor =
  string * annterm                             (* id, type *)