Change default for notations with variables bound to both terms and binders.

For compatibility, the default is to parse as ident and not as pattern.

7 files changed, 29 insertions, 10 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 158ac24b2e..694bec8972 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -273,8 +273,8 @@ let error_expect_binder_notation_type ?loc id =
 
 let set_var_scope ?loc id istermvar (tmp_scope,subscopes as scopes) ntnvars =
   try
-    let isonlybinding,idscopes,typ = Id.Map.find id ntnvars in
-    if istermvar then isonlybinding := false;
+    let used_as_binder,idscopes,typ = Id.Map.find id ntnvars in
+    if not istermvar then used_as_binder := true;
     let () = if istermvar then
       (* scopes have no effect on the interpretation of identifiers *)
       begin match !idscopes with
@@ -1997,7 +1997,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
         | Some gen ->
           let (ltacvars, ntnvars) = lvar in
           (* Preventively declare notation variables in ltac as non-bindings *)
-          Id.Map.iter (fun x (isonlybinding,_,_) -> isonlybinding := false) ntnvars;
+          Id.Map.iter (fun x (used_as_binder,_,_) -> used_as_binder := false) ntnvars;
           let ntnvars = Id.Map.domain ntnvars in
           let extra = ltacvars.ltac_extra in
           let lvars = Id.Set.union ltacvars.ltac_bound ltacvars.ltac_vars in
@@ -2302,7 +2302,7 @@ let intern_constr_pattern env ?(as_type=false) ?(ltacvars=empty_ltac_sign) c =
 
 let interp_notation_constr env ?(impls=empty_internalization_env) nenv a =
   (* [vl] is intended to remember the scope of the free variables of [a] *)
-  let vl = Id.Map.map (fun typ -> (ref true, ref None, typ)) nenv.ninterp_var_type in
+  let vl = Id.Map.map (fun typ -> (ref false, ref None, typ)) nenv.ninterp_var_type in
   let impls = Id.Map.fold (fun id _ impls -> Id.Map.remove id impls) nenv.ninterp_var_type impls in
   let c = internalize (Global.env()) {ids = extract_ids env; unb = false;
 						tmp_scope = None; scopes = []; impls = impls}
@@ -2313,8 +2313,8 @@ let interp_notation_constr env ?(impls=empty_internalization_env) nenv a =
   (* binding and bound *)
   let out_scope = function None -> None,[] | Some (a,l) -> a,l in
   let unused = match reversible with NonInjective ids -> ids | _ -> [] in
-  let vars = Id.Map.mapi (fun id (isonlybinding, sc, typ) ->
-    (!isonlybinding && not (List.mem_f Id.equal id unused), out_scope !sc)) vl in
+  let vars = Id.Map.mapi (fun id (used_as_binder, sc, typ) ->
+    (!used_as_binder && not (List.mem_f Id.equal id unused), out_scope !sc)) vl in
   (* Returns [a] and the ordered list of variables with their scopes *)
   vars, a, reversible
 
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index 0b5009e26b..d16c9bb802 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -214,7 +214,7 @@ type proof_expr =
 
 type syntax_modifier =
   | SetItemLevel of string list * Extend.production_level
-  | SetItemLevelAsBinder of string list * Extend.constr_as_binder_kind * Extend.production_level
+  | SetItemLevelAsBinder of string list * Extend.constr_as_binder_kind * Extend.production_level option
   | SetLevel of int
   | SetAssoc of Extend.gram_assoc
   | SetEntryType of string * Extend.simple_constr_prod_entry_key
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index cca1b29898..d90fd3eb70 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -1174,7 +1174,8 @@ GEXTEND Gram
       | x = IDENT; ","; l = LIST1 [id = IDENT -> id ] SEP ","; "at";
         lev = level -> SetItemLevel (x::l,lev)
       | x = IDENT; "at"; lev = level -> SetItemLevel ([x],lev)
-      | x = IDENT; "at"; lev = level; b = constr_as_binder_kind -> SetItemLevelAsBinder ([x],b,lev)
+      | x = IDENT; "at"; lev = level; b = constr_as_binder_kind -> SetItemLevelAsBinder ([x],b,Some lev)
+      | x = IDENT; b = constr_as_binder_kind -> SetItemLevelAsBinder ([x],b,None)
       | x = IDENT; typ = syntax_extension_type -> SetEntryType (x,typ)
     ] ]
   ;
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 2fc7843eda..31c0d20f32 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -383,7 +383,7 @@ open Decl_kinds
       prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level n
     | SetItemLevelAsBinder (l,bk,n) ->
       prlist_with_sep sep_v2 str l ++
-      spc() ++ pr_at_level n ++ spc() ++ pr_constr_as_binder_kind bk
+      spc() ++ pr_at_level_opt n ++ spc() ++ pr_constr_as_binder_kind bk
     | SetLevel n -> pr_at_level (NumLevel n)
     | SetAssoc LeftA -> keyword "left associativity"
     | SetAssoc RightA -> keyword "right associativity"
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 3fd4c1c311..436e97e9fb 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -219,3 +219,9 @@ fun p : nat => if p is S n then n else 0
      : nat -> nat
 fun p : comparison => if p is Lt then 1 else 0
      : comparison -> nat
+fun S : nat => [S | S + S]
+     : nat -> nat * (nat -> nat)
+fun N : nat => [N | N + 0]
+     : nat -> nat * (nat -> nat)
+fun S : nat => [[S | S + S]]
+     : nat -> nat * (nat -> nat)
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 9ea218481e..df3d86793f 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -389,3 +389,15 @@ Notation "'if' c 'is' p 'then' u 'else' v" :=
   (at level 200, p pattern at level 100).
 Check fun p => if p is S n then n else 0.
 Check fun p => if p is Lt then 1 else 0.
+
+(* Check that mixed binders and terms defaults to ident and not pattern *)
+Module E.
+  (* First without an indirection *)
+Notation "[ n | t ]" := (n, (fun n : nat => t)).
+Check fun S : nat => [ S | S+S ].
+Check fun N : nat => (N, (fun n => n+0)). (* another test in passing *)
+  (* Then with an indirection *)
+Notation "[[ n | p | t ]]" := (n, (fun p : nat => t)).
+Notation "[[ n | t ]]" := [[ n | n | t ]].
+Check fun S : nat => [[ S | S+S ]].
+End E.
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 524c9b32b1..bcffe640cf 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -831,7 +831,7 @@ let interp_modifiers modl = let open NotationMods in
         if Id.List.mem_assoc id acc.etyps then
           user_err ~hdr:"Metasyntax.interp_modifiers"
             (str s ++ str " is already assigned to an entry or constr level.");
-        let typ = ETConstrAsBinder (bk,Some n) in
+        let typ = ETConstrAsBinder (bk,n) in
         interp { acc with etyps = (id,typ)::acc.etyps; } (SetItemLevelAsBinder (idl,bk,n)::l)
     | SetLevel n :: l ->
         interp { acc with level = Some n; } l