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

5 files changed, 13 insertions, 5 deletions

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