Faire que les niveaux de tactiques soient correctement parsés par ARGUMENT EXTEND et TACTIC EXTEND

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

1 files changed, 16 insertions, 13 deletions

diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4
index eef16b1eb..ac1f3f050 100644
--- a/parsing/q_util.ml4
+++ b/parsing/q_util.ml4
@@ -84,24 +84,27 @@ let rec interp_entry_name loc s =
     OptArgType t, <:expr< Gramext.Sopt $g$ >>
   else
     let s = if s = "hyp" then "var" else s in
-    let t, se =
-      if tactic_genarg_level s <> None then
-        Some (ExtraArgType s), <:expr< Tactic. tactic >>
-      else
+    let t, se, lev =
+      match tactic_genarg_level s with
+	| 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$ >>
+	| Some _ as x -> x, <:expr< Prim. $lid:s$ >>, None
 	| None -> 
       match Pcoq.entry_type (Pcoq.get_univ "constr") s with
-	| Some _ as x -> x, <:expr< Constr. $lid:s$ >>
+	| Some _ as x -> x, <:expr< Constr. $lid:s$ >>, None
 	| None -> 
       match Pcoq.entry_type (Pcoq.get_univ "tactic") s with
-	| Some _ as x -> x, <:expr< Tactic. $lid:s$ >>
-	| None -> None, <:expr< $lid:s$ >> in
+	| Some _ as x -> x, <:expr< Tactic. $lid:s$ >>, None
+	| None -> None, <:expr< $lid:s$ >>, None in
     let t =
       match t with
 	| Some t -> t
-	| None ->
-(*	    Pp.warning_with Pp_control.err_ft
-            ("Unknown primitive grammar entry: "^s);*)
-	    ExtraArgType s
-    in t, <:expr< Gramext.Snterm (Pcoq.Gram.Entry.obj $se$) >>
+	| None -> ExtraArgType s in
+    let entry = match lev with
+      | Some n ->
+	  let s = string_of_int n in
+	  <:expr< Gramext.Snterml (Pcoq.Gram.Entry.obj $se$, $str:s$) >>
+      | None -> 
+	  <:expr< Gramext.Snterm (Pcoq.Gram.Entry.obj $se$) >>
+    in t, entry