3 files changed, 9 insertions, 17 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index d95e254c8..c567a2f94 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -224,11 +224,10 @@ let add_infix assoc n inf pr =
     errorlabstrm "Vernacentries.infix_grammar_entry"
       [< 'sTR"Associativity Precedence must be 6,7,8 or 9." >];
   (* check the grammar entry *)
-  let prefast = Termast.ast_of_ref pr in
-  let prefname = (Names.string_of_path (Global.sp_of_global pr))^"_infix" in
-  let gram_rule = gram_infix assoc n (split inf) prefname prefast in
+  let prefname = inf^"_infix" in
+  let gram_rule = gram_infix assoc n (split inf) prefname pr in
   (* check the syntax entry *)
-  let syntax_rule = infix_syntax_entry assoc n inf prefname prefast in
+  let syntax_rule = infix_syntax_entry assoc n inf prefname pr in
   Lib.add_anonymous_leaf (inInfix(gram_rule,syntax_rule))
 
 (* Distfix *)
@@ -272,8 +271,7 @@ let distfix assoc n sl fname astf  =
       ]
   }
 
-let add_distfix a n df f =
-  let fname = (Names.string_of_path (Global.sp_of_global f))^"_distfix" in
-  let astf = Termast.ast_of_ref f in
+let add_distfix a n df astf =
+  let fname = df^"_distfix" in
   Lib.add_anonymous_leaf (inInfix(distfix a n (split df) fname astf, []))
 
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index 08fb2800d..b51a9a43d 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -1,12 +1,6 @@
 
 (*i $Id$ i*)
 
-(*i*)
-open Extend
-open Names
-open Term
-(*i*)
-
 (* Adding grammar and pretty-printing objects in the environment *)
 
 val add_syntax_obj : string -> Coqast.t list -> unit
@@ -15,8 +9,8 @@ val add_grammar_obj : string -> Coqast.t list -> unit
 val add_token_obj : string -> unit
 
 val add_infix :
-  Gramext.g_assoc option -> int -> string -> global_reference -> unit
+  Gramext.g_assoc option -> int -> string -> Coqast.t -> unit
 val add_distfix :
-  Gramext.g_assoc option -> int -> string -> global_reference -> unit
+  Gramext.g_assoc option -> int -> string -> Coqast.t -> unit
 
 val print_grammar : string -> string -> unit
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 11e65b934..02d2ce6a3 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1469,8 +1469,8 @@ let _ =
   add "INFIX"
     (function
        | [VARG_AST assoc; VARG_NUMBER n; VARG_STRING inf; VARG_QUALID pref] ->
+	   let ref = Termast.ast_of_qualid pref in
            (fun () ->
-	      let ref = global dummy_loc pref in
 	      Metasyntax.add_infix (Extend.gram_assoc assoc) n inf ref)
        | _ -> bad_vernac_args "INFIX")
 
@@ -1478,8 +1478,8 @@ let _ =
   add "DISTFIX"
     (function
        | [VARG_AST assoc; VARG_NUMBER n; VARG_STRING s; VARG_QUALID pref] ->
+	   let ref = Termast.ast_of_qualid pref in
            (fun () ->
-	      let ref = global dummy_loc pref in
               Metasyntax.add_distfix (Extend.gram_assoc assoc) n s ref)
        | _ -> bad_vernac_args "DISTFIX")