diff options
| author | Pierre Letouzey | 2014-12-09 12:48:32 +0100 |
|---|---|---|
| committer | Pierre Letouzey | 2014-12-09 14:27:21 +0100 |
| commit | af84e080ff674a3d5cf2cf88874ddb6ebaf38ecf (patch) | |
| tree | b8325cd8ce34dd2dcfba2792a0123cf8c46ab703 /tactics | |
| parent | 9c24cecec3a7381cd924c56ca50c77a49750e2e5 (diff) | |
Switch the few remaining iso-latin-1 files to utf8
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/elim.ml | 6 | ||||
| -rw-r--r-- | tactics/leminv.ml | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/tactics/elim.ml b/tactics/elim.ml index ba413d4105..c83441894b 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 *) diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 7eb81c3f48..d0946e2ad7 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -242,7 +242,7 @@ let add_inversion_lemma_exn na com comsort bool tac = try add_inversion_lemma na env sigma c sort bool tac with - | UserError ("Case analysis",s) -> (* référence à Indrec *) + | UserError ("Case analysis",s) -> (* Reference to Indrec *) errorlabstrm "Inv needs Nodep Prop Set" s (* ================================= *) |