Compatibilité hyp=var dans Tactic Notation + nettoyage

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

3 files changed, 10 insertions, 10 deletions

diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index bc351cbaa8..774034f702 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -196,18 +196,19 @@ let find_index s t =
   if s <> t or n = None then raise Not_found;
   out_some n
 
-let rec interp_entry_name up_level u s =
+let rec interp_entry_name up_level s =
   let l = String.length s in
   if l > 8 & String.sub s 0 3 = "ne_" & String.sub s (l-5) 5 = "_list" then
-    let t, g = interp_entry_name up_level u (String.sub s 3 (l-8)) in
+    let t, g = interp_entry_name up_level (String.sub s 3 (l-8)) in
     List1ArgType t, Gramext.Slist1 g
   else if l > 5 & String.sub s (l-5) 5 = "_list" then
-    let t, g = interp_entry_name up_level u (String.sub s 0 (l-5)) in
+    let t, g = interp_entry_name up_level (String.sub s 0 (l-5)) in
     List0ArgType t, Gramext.Slist0 g
   else if l > 4 & String.sub s (l-4) 4 = "_opt" then
-    let t, g = interp_entry_name up_level u (String.sub s 0 (l-4)) in
+    let t, g = interp_entry_name up_level (String.sub s 0 (l-4)) in
     OptArgType t, Gramext.Sopt g
   else
+    let s = if s = "hyp" then "var" else s in
     try 
       let i = find_index "tactic" s in
       ExtraArgType s, 
@@ -228,10 +229,10 @@ let rec interp_entry_name up_level u s =
     let t = type_of_typed_entry e in
     t,Gramext.Snterm (Pcoq.Gram.Entry.obj o)
 
-let make_vprod_item n univ = function
+let make_vprod_item n = function
   | VTerm s -> (Gramext.Stoken (Lexer.terminal s), None)
   | VNonTerm (loc, nt, po) ->
-      let (etyp, e) = interp_entry_name n univ nt in
+      let (etyp, e) = interp_entry_name n nt in
       e, option_map (fun p -> (p,etyp)) po
 
 let get_tactic_entry n =
@@ -249,7 +250,7 @@ let head_is_ident = function VTerm _::_ -> true | _ -> false
 let add_tactic_entry (key,lev,prods,tac) =
   let univ = get_univ "tactic" in
   let entry, pos = get_tactic_entry lev in
-  let mkprod = make_vprod_item lev "tactic" in
+  let mkprod = make_vprod_item lev in
   let rules = 
     if lev = 0 then begin
       if not (head_is_ident prods) then
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli
index 92efd0824d..8de2af4ec6 100644
--- a/parsing/egrammar.mli
+++ b/parsing/egrammar.mli
@@ -61,8 +61,7 @@ val get_extend_vernac_grammars :
 (*
 val reset_extend_grammars_v8 : unit -> unit
 *)
-val interp_entry_name : int -> string -> string -> 
-  entry_type * Token.t Gramext.g_symbol
+val interp_entry_name : int -> string -> entry_type * Token.t Gramext.g_symbol
 
 val recover_notation_grammar :
   notation -> (precedence * tolerability list) -> notation_grammar
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 4fab315da0..a22f99c39c 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -50,7 +50,7 @@ let make_terminal_status = function
 let rec make_tags lev = function
   | VTerm s :: l -> make_tags lev l
   | VNonTerm (loc, nt, po) :: l ->
-      let (etyp, _) = Egrammar.interp_entry_name lev "tactic" nt in
+      let (etyp, _) = Egrammar.interp_entry_name lev nt in
       etyp :: make_tags lev l
   | [] -> []