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

3 files changed, 3 insertions, 3 deletions

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