From 6d3d0d2f9a6257430e4039b1c69af6a0e81e133a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 26 Nov 2003 23:57:51 +0000
Subject: 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
---
 translate/pptacticnew.ml | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index 8972683fd6..bad3ac90f2 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 = 
-- 
cgit v1.2.3