Comments improved.

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index b2f6dd8f1c87985d8bf3672e78595067c6cf319f..f0bccf6eaa62f1d5cea5567214035fd3026458b2 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