Fixing bug #5526,allow nonlinear variables in Notation patterns

4 files changed, 24 insertions, 11 deletions

diff --git a/test-suite/bugs/closed/5526.v b/test-suite/bugs/closed/5526.v
new file mode 100644
index 000000000..88f219be3
--- /dev/null
+++ b/test-suite/bugs/closed/5526.v
@@ -0,0 +1,3 @@
+Fail Notation "x === x" := (eq_refl x) (at level 10).
+Reserved Notation "x === x" (only printing, at level 10).
+Notation "x === x" := (eq_refl x) (only printing).
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 360f37967..0cb870c57 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -98,3 +98,7 @@ fun n : nat => foo4 n (fun _ y : nat => ETA z : nat, (fun _ : nat => y = 0))
      : nat -> Prop
 tele (t : Type) '(y, z) (x : t0) := tt
      : forall t : Type, nat * nat -> t -> fpack
+fun x : ?A => x === x
+     : forall x : ?A, x = x
+where
+?A : [x : ?A |- Type] (x cannot be used)
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 4b8bfe312..5676fe8c7 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -139,3 +139,9 @@ Notation "'tele' x .. z := b" :=
   (at level 85, x binder, z binder).
 
 Check tele (t:Type) '((y,z):nat*nat) (x:t) := tt.
+
+(**********************************************************************)
+(* Test printing of #5526                                             *)
+
+Notation "x === x" := (eq_refl x) (only printing, at level 10).
+Check (fun x => eq_refl x).
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 349c05a38..6ad5182e2 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -294,22 +294,22 @@ let is_numeral symbs =
   | _ ->
       false
 
-let rec get_notation_vars = function
+let rec get_notation_vars onlyprint = function
   | [] -> []
   | NonTerminal id :: sl ->
-      let vars = get_notation_vars sl in
+      let vars = get_notation_vars onlyprint sl in
       if Id.equal id ldots_var then vars else
-	if Id.List.mem id vars then
+	(* don't check for nonlinearity if printing only, see Bug 5526 *)
+	if not onlyprint && Id.List.mem id vars then 
 	  errorlabstrm "Metasyntax.get_notation_vars"
             (str "Variable " ++ pr_id id ++ str " occurs more than once.")
-	else
-          id::vars
-  | (Terminal _ | Break _) :: sl -> get_notation_vars sl
+	else id::vars
+  | (Terminal _ | Break _) :: sl -> get_notation_vars onlyprint sl
   | SProdList _ :: _ -> assert false
 
-let analyze_notation_tokens l =
+let analyze_notation_tokens ~onlyprint l =
   let l = raw_analyze_notation_tokens l in
-  let vars = get_notation_vars l in
+  let vars = get_notation_vars onlyprint l in
   let recvars,l = interp_list_parser [] l in
   recvars, List.subtract Id.equal vars (List.map snd recvars), l
 
@@ -1016,7 +1016,7 @@ let compute_syntax_data df modifiers =
   if onlyprint && onlyparse then error "A notation cannot be both 'only printing' and 'only parsing'.";
   let assoc = match assoc with None -> (* default *) Some NonA | a -> a in
   let toks = split_notation_string df in
-  let (recvars,mainvars,symbols) = analyze_notation_tokens toks in
+  let (recvars,mainvars,symbols) = analyze_notation_tokens onlyprint toks in
   let _ = check_useless_entry_types recvars mainvars etyps in
   let _ = check_binder_type recvars etyps in
   let ntn_for_interp = make_notation_key symbols in
@@ -1240,7 +1240,7 @@ let add_notation_in_scope local df c mods scope =
 
 let add_notation_interpretation_core local df ?(impls=empty_internalization_env) c scope onlyparse onlyprint compat =
   let dfs = split_notation_string df in
-  let (recvars,mainvars,symbs) = analyze_notation_tokens dfs in
+  let (recvars,mainvars,symbs) = analyze_notation_tokens onlyprint dfs in
   (* Recover types of variables and pa/pp rules; redeclare them if needed *)
   let i_typs, onlyprint = if not (is_numeral symbs) then begin
     let i_typs,sy_rules,onlyprint' = recover_notation_syntax (make_notation_key symbs) in
@@ -1317,7 +1317,7 @@ let add_notation local c ((loc,df),modifiers) sc =
 let add_notation_extra_printing_rule df k v =
   let notk = 
     let dfs = split_notation_string df in
-    let _,_, symbs = analyze_notation_tokens dfs in
+    let _,_, symbs = analyze_notation_tokens ~onlyprint:true dfs in
     make_notation_key symbs in
   Notation.add_notation_extra_printing_rule notk k v