From 33c27a9941fb0ba8be59e041140aa873b4c4d700 Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 12 Aug 2005 06:48:20 +0000
Subject: [PATCH] improved some comments
---
helm/ocaml/cic/cic.ml | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
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 , *)
--
2.39.2