diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-26 23:57:51 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-26 23:57:51 +0000 |
| commit | 6d3d0d2f9a6257430e4039b1c69af6a0e81e133a (patch) | |
| tree | 6229f4d8f90ea8f42cc636854c6eb08a33d6d028 /translate | |
| parent | a3b28cad6d5a0cb731c6f2e54980ffec59aed371 (diff) | |
Renommage de tactiques ltac coincidant avec certaines tactiques primitives
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5000 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'translate')
| -rw-r--r-- | translate/pptacticnew.ml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml index 8972683fd..bad3ac90f 100644 --- a/translate/pptacticnew.ml +++ b/translate/pptacticnew.ml @@ -130,6 +130,12 @@ let translate_v7_ltac = function | "SimplAllMonoms" -> "simpl_all_monomials" | "AssocDistrib" -> "assoc_distrib" | "NowShow" -> "now_show" + | ("subst"|"simpl"|"elim"|"destruct"|"apply"|"intro" (* ... *)) as x -> + let x' = x^"_" in + msgerrnl + (str ("Warning: '"^ + x^"' is now a primitive tactic; it has been translated to '"^x'^"'")); + x' | x -> x let id_of_ltac_v7_id id = |