diff options
| author | herbelin | 2000-08-28 10:07:21 +0000 |
|---|---|---|
| committer | herbelin | 2000-08-28 10:07:21 +0000 |
| commit | 1c8eaac415b43ec27aa81afdc39837c14fb2d92c (patch) | |
| tree | 2e66c7e5a4dbb2a37d61cdd16393bf526d7671fc | |
| parent | 9e6b313fbb13f3673192e816e1360a4f5e7e92fd (diff) | |
cosmétique
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@582 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/refine.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |