Notations: Do not consider a non-occurring variable as a binder-only variable.

2 files changed, 11 insertions, 4 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index b52a28029..2761b6528 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2170,8 +2170,9 @@ let interp_notation_constr env ?(impls=empty_internalization_env) nenv a =
   (* Splits variables into those that are binding, bound, or both *)
   (* binding and bound *)
   let out_scope = function None -> None,[] | Some (a,l) -> a,l in
-  let vars = Id.Map.map (fun (isonlybinding, sc, typ) ->
-    (!isonlybinding, out_scope !sc, typ)) vl 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, typ)) vl in
   (* Returns [a] and the ordered list of variables with their scopes *)
   vars, a, reversible
 
diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index 2655b651a..08d904cea 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -92,8 +92,7 @@ Check ##### 0 _ 0%bool 0%bool : prod' bool bool.
 Check fun A (x :prod' bool A) => match x with ##### 0 _ y 0%bool => 2 | _ => 1 end.
 
 (* 10. Check computation of binding variable through other notations *)
-(* i should be detected as binding variable and the scopes not being checked *)
-
+(* it should be detected as binding variable and the scopes not being checked *)
 Notation "'FUNNAT' i => t" := (fun i : nat => i = t) (at level 200).
 Notation "'Funnat' i => t" := (FUNNAT i => t + i%nat) (at level 200).
 
@@ -105,3 +104,10 @@ Notation "[:: x1 ; .. ; xn ]" := (cons x1 .. (cons xn nil) ..).
 Check [:: 1 ; 2 ; 3 ].
 Check [:: 1 ; 2 ; 3 & nil ]. (* was failing *)
 End A.
+
+(* 12. Preventively check that a variable which does not occur can be instantiated *)
+(* by any term. In particular, it should not be restricted to a binder *)
+Module M12.
+Notation "N ++ x" := (S x) (only parsing).
+Check 2 ++ 0.
+End M12.