From 1c8eaac415b43ec27aa81afdc39837c14fb2d92c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 28 Aug 2000 10:07:21 +0000
Subject: cosmétique

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@582 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/refine.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/refine.ml b/tactics/refine.ml
index 8a43cff935..e4a36a5251 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -21,7 +21,7 @@
 (*  Pour cela, on procède de la manière suivante :
  *
  *  1. Un terme de preuve incomplet est un terme contenant des variables
- *     existentielles (XTRA "ISEVAR") i.e. "?" en syntaxe concrète.
+ *     existentielles Evar i.e. "?" en syntaxe concrète.
  *     La résolution de ces variables n'est plus nécessairement totale
  *     (ise_resolve called with fail_evar=false) et les variables
  *     existentielles restantes sont remplacées par des méta-variables
-- 
cgit v1.2.3