diff options
| -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 |