From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 12 Aug 2005 06:48:20 +0000 (+0000)
Subject: improved some comments
X-Git-Tag: V_0_1_1_1~3
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=33c27a9941fb0ba8be59e041140aa873b4c4d700;p=helm.git

improved some comments
---

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index 1c2bf8df0..aacaabda9 100644
--- a/helm/ocaml/cic/cic.ml
+++ b/helm/ocaml/cic/cic.ml
@@ -111,7 +111,7 @@ and obj =
     UriManager.uri list * attribute list          (*  parameters              *)
  | Variable of string * term option * term *      (* name, body, type         *)
     UriManager.uri list * attribute list          (* parameters               *)
- | CurrentProof of string * metasenv * term *     (* name, conjectures, value,*)
+ | CurrentProof of string * metasenv * term *     (* name, conjectures, body, *)
     term * UriManager.uri list * attribute list   (*  type, parameters        *)
  | InductiveDefinition of inductiveType list *    (* inductive types,         *)
     UriManager.uri list * int * attribute list    (*  params, left params no  *)
@@ -179,7 +179,7 @@ and annobj =
     UriManager.uri list * attribute list            (*  parameters      *)
  | ACurrentProof of id * id *
     string * annmetasenv *                          (*  name, conjectures,    *)
-    annterm * annterm * UriManager.uri list *       (*  value,type,parameters *)
+    annterm * annterm * UriManager.uri list *       (*  body,type,parameters  *)
     attribute list
  | AInductiveDefinition of id *
     anninductiveType list *                         (* inductive types ,      *)