From 33c27a9941fb0ba8be59e041140aa873b4c4d700 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli 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