From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 15 Nov 2002 18:41:34 +0000 (+0000)
Subject: Comments improved.
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b6c2107995066dea2b31fe9f760af3cac2d8cebc;p=helm.git

Comments improved.
---

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index b2f6dd8f1..f0bccf6ea 100644
--- 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