diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-12-09 12:48:32 +0100 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-12-09 14:27:21 +0100 |
| commit | af84e080ff674a3d5cf2cf88874ddb6ebaf38ecf (patch) | |
| tree | b8325cd8ce34dd2dcfba2792a0123cf8c46ab703 /tactics/elim.ml | |
| parent | 9c24cecec3a7381cd924c56ca50c77a49750e2e5 (diff) | |
Switch the few remaining iso-latin-1 files to utf8
Diffstat (limited to 'tactics/elim.ml')
| -rw-r--r-- | tactics/elim.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/elim.ml b/tactics/elim.ml index ba413d410..c83441894 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -77,10 +77,10 @@ and general_decompose_aux recognizer id = (ids_of_named_context bas.Tacticals.assums)))) id -(* Faudrait ajouter un COMPLETE pour que l'hypothèse créée ne reste - pas si aucune élimination n'est possible *) +(* We should add a COMPLETE to be sure that the created hypothesis + doesn't stay if no elimination is possible *) -(* Meilleures stratégies mais perte de compatibilité *) +(* Best strategies but loss of compatibility *) let tmphyp_name = Id.of_string "_TmpHyp" let up_to_delta = ref false (* true *) |