diff options
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 (* ================================= *) |