Add support for "Infix ... := constr" instead of just "Infix ... := ref".

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

5 files changed, 6 insertions, 6 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 41ac3b5104..ea686e5a3d 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -811,7 +811,7 @@ GEXTEND Gram
 	 VernacArgumentsScope (use_non_locality (),qid,scl)
 
      | IDENT "Infix"; local = obsolete_locality;
-	 op = ne_string; ":="; p = global; 
+	 op = ne_string; ":="; p = constr; 
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
          VernacInfix (enforce_locality_of local,(op,modl),p,sc)
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 049a227eb0..3bf2f0ede2 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -508,7 +508,7 @@ let rec pr_vernac = function
     ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]"
   | VernacInfix (local,(s,mv),q,sn) -> (* A Verifier *)
       hov 0 (hov 0 (str"Infix " ++ pr_locality local
-      ++ qs s ++ str " :=" ++ spc() ++ pr_reference q) ++
+      ++ qs s ++ str " :=" ++ pr_constrarg q) ++
       pr_syntax_modifiers mv ++
       (match sn with
     | None -> mt()
@@ -521,7 +521,7 @@ let rec pr_vernac = function
           let s' = String.sub s 1 (n-2) in
           if String.contains s' '\'' then qs s else str s'
 	else qs s in
-      hov 2( str"Notation" ++ spc() ++ pr_locality local ++ ps ++
+      hov 2 (str"Notation" ++ spc() ++ pr_locality local ++ ps ++
       str " :=" ++ pr_constrarg c ++ pr_syntax_modifiers l ++
       (match opt with
         | None -> mt()
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index e6c469974b..adf3e93a4d 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -1011,7 +1011,7 @@ let add_infix local (inf,modifiers) pr sc =
   check_infix_modifiers modifiers;
   (* check the precedence *)
   let metas = [inject_var "x"; inject_var "y"] in
-  let c = mkAppC (mkRefC pr,metas) in
+  let c = mkAppC (pr,metas) in
   let df = "x "^(quote_notation_token inf)^" y" in
   add_notation local c (df,modifiers) sc
 
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index 4973cdfe6d..29dbcb4daa 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -29,7 +29,7 @@ val add_tactic_notation :
 (* Adding a (constr) notation in the environment*)
 
 val add_infix : locality_flag -> (string * syntax_modifier list) ->
-  reference -> scope_name option -> unit
+  constr_expr -> scope_name option -> unit
 
 val add_notation : locality_flag -> constr_expr ->
   (string * syntax_modifier list) -> scope_name option -> unit
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index b38277cca1..ee86f982e8 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -206,7 +206,7 @@ type vernac_expr =
   | VernacBindScope of scope_name * class_rawexpr list
   | VernacArgumentsScope of locality_flag * lreference * scope_name option list
   | VernacInfix of locality_flag * (lstring * syntax_modifier list) *
-      lreference * scope_name option
+      constr_expr * scope_name option
   | VernacNotation of
       locality_flag * constr_expr * (lstring * syntax_modifier list) *
       scope_name option