gestion speciale du niveau 5 des ltac

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

7 files changed, 20 insertions, 9 deletions

diff --git a/CHANGES b/CHANGES
index 2319f1c0ac..909de4277a 100644
--- a/CHANGES
+++ b/CHANGES
@@ -21,7 +21,9 @@ Language and commands
 
 Tactics
 
-- Improved implementation of the ring and field tactics.
+- Improved implementation of the ring and field tactics. For compatibility
+  reasons, the previous tactics are renamed as legacy ring and legacy field,
+  but should be considered as deprecated.
 - New declarative mathematical proof language.
 - Support for argument lists of arbitrary length in Tactic Notation.
 - [rewrite ... in H] now fails if [H] is used either in an hypothesis
@@ -90,9 +92,8 @@ Tactics
   setoid_symmetry, setoid_transitivity, setoid_reflexivity and autorewite).
   New syntax for declaring relations and morphisms (old syntax still working
   with minor modifications, but deprecated).
-- New implementation of the ring tactic with a built-in notion of coefficients
-  and a better usage of setoids. Previous implementation kept for compatibility
-  but is deprecated.
+- New implementation (still experimental) of the ring tactic with a built-in
+  notion of coefficients and a better usage of setoids.
 - New conversion tactic "vm_compute": evaluates the goal (or an hypothesis)
   with a call-by-value strategy, using the compiled version of terms. 
 - When rewriting H where H is not directly a Coq equality, search first H for 
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 774034f702..e28890cee7 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -212,8 +212,8 @@ let rec interp_entry_name up_level s =
     try 
       let i = find_index "tactic" s in
       ExtraArgType s, 
-      if i=up_level then Gramext.Sself else
-      if i=up_level-1 then Gramext.Snext else
+      if up_level<>5 && i=up_level then Gramext.Sself else
+      if up_level<>5 && i=up_level-1 then Gramext.Snext else
       Gramext.Snterml(Pcoq.Gram.Entry.obj Tactic.tactic_expr,string_of_int i)
     with Not_found ->
     let e = 
@@ -238,7 +238,9 @@ let make_vprod_item n = function
 let get_tactic_entry n =
   if n = 0 then
     weaken_entry Tactic.simple_tactic, None
-  else if 1<=n && n<=5 then
+  else if n = 5 then
+    weaken_entry Tactic.binder_tactic, None
+  else if 1<=n && n<5 then
     weaken_entry Tactic.tactic_expr, Some (Gramext.Level (string_of_int n))
   else 
     error ("Invalid Tactic Notation level: "^(string_of_int n))
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 31e5ff906c..428c9efb7f 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -43,7 +43,8 @@ let tacarg_of_expr = function
 (* Tactics grammar rules *)
 
 GEXTEND Gram
-  GLOBAL: tactic Vernac_.command tactic_expr tactic_arg constr_may_eval;
+  GLOBAL: tactic Vernac_.command tactic_expr binder_tactic tactic_arg
+          constr_may_eval;
 
   tactic_expr:
     [ "5" RIGHTA
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index c3a571a137..ecbc2ef6c0 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -430,6 +430,7 @@ module Tactic =
     (* Main entries for ltac *)
     let tactic_arg = Gram.Entry.create "tactic:tactic_arg"
     let tactic_expr = Gram.Entry.create "tactic:tactic_expr"
+    let binder_tactic = Gram.Entry.create "tactic:binder_tactic"
 
     let tactic = make_gen_entry utactic (rawwit_tactic tactic_main_level) "tactic"
 
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 27239599ca..b0f997d24e 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -184,6 +184,7 @@ module Tactic :
     val simple_intropattern : Genarg.intro_pattern_expr Gram.Entry.e
     val tactic_arg : raw_tactic_arg Gram.Entry.e
     val tactic_expr : raw_tactic_expr Gram.Entry.e
+    val binder_tactic : raw_tactic_expr Gram.Entry.e
     val tactic : raw_tactic_expr Gram.Entry.e
     val tactic_eoi : raw_tactic_expr Gram.Entry.e
   end
diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4
index d4b4682fee..f7ea7ee468 100644
--- a/parsing/q_util.ml4
+++ b/parsing/q_util.ml4
@@ -107,7 +107,10 @@ let rec interp_entry_name loc s sep =
     let s = if s = "hyp" then "var" else s in
     let t, se, lev =
       match tactic_genarg_level s with
-	| Some n -> Some (ExtraArgType s), <:expr< Tactic. tactic_expr >>, Some n
+        | Some 5 ->
+            Some (ExtraArgType s), <:expr< Tactic. binder_tactic >>, None
+	| Some n ->
+            Some (ExtraArgType s), <:expr< Tactic. tactic_expr >>, Some n
 	| None ->
       match Pcoq.entry_type (Pcoq.get_univ "prim") s with
 	| Some _ as x -> x, <:expr< Prim. $lid:s$ >>, None
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 18ff746f1c..eaa750ab3d 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -112,6 +112,8 @@ let print_grammar univ = function
   | "tactic" -> 
       msgnl (str "Entry tactic_expr is");
       Gram.Entry.print Pcoq.Tactic.tactic_expr;
+      msgnl (str "Entry binder_tactic is");
+      Gram.Entry.print Pcoq.Tactic.binder_tactic;
       msgnl (str "Entry simple_tactic is");
       Gram.Entry.print Pcoq.Tactic.simple_tactic;
   | "vernac" ->