Suppression des parseurs et printeurs v7; suppression du traducteur (mcanismes de renommage des noms de constantes, de module, de ltac et de certaines variables lies de lemmes et de tactiques, mcanisme d'ajout d'arguments implicites, etc.)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7734 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 6 deletions

diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index ef3561a70..e2edbd8ba 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -632,17 +632,17 @@ let pcoq_hook = {
 }
 
 
-TACTIC EXTEND Pbp
-| [ "Pbp" ident_opt(idopt) natural_list(nl) ] -> 
+TACTIC EXTEND pbp
+| [ "pbp" ident_opt(idopt) natural_list(nl) ] -> 
     [ if_pcoq pbp_tac_pcoq idopt nl ]
 END
 
-TACTIC EXTEND CtDebugTac
-| [ "DebugTac" tactic(t) ] -> [ if_pcoq debug_tac2_pcoq (fst t) ]
+TACTIC EXTEND ct_debugtac
+| [ "debugtac" tactic(t) ] -> [ if_pcoq debug_tac2_pcoq (fst t) ]
 END
 
-TACTIC EXTEND CtDebugTac2
-| [ "DebugTac2" tactic(t) ] -> [ if_pcoq debug_tac2_pcoq (fst t) ]
+TACTIC EXTEND ct_debugtac2
+| [ "debugtac2" tactic(t) ] -> [ if_pcoq debug_tac2_pcoq (fst t) ]
 END