Syntax error in Search underscore

[yaitskov]

Hi,

Map module in SF book use underscore (_) as part of a notation.
Search command breaks. The underscore in a notation is not best choice but the symbol is allowed to be used there so bug looks legit until then.

Bug.v:

Definition total_map (A : Type) := nat -> A.
Definition t_empty {A : Type} (v : A) : total_map A := (fun _ => v).
Definition t_update {A : Type} (m : total_map A) (x : nat) (v : A) :=  fun x' => m x'.
Notation "'_' '!->' v" := (t_empty v) (at level 100, right associativity).
Notation "x '!->' v ';' m" := (t_update m x v) (at level 100, v at next level, right associativity).
Lemma t_update_eq : forall (A : Type) (m : total_map A) x v, (x !-> v ; m) x = v. Admitted.
Search (_ !-> _ ; _).

$ rocq c Bug.v 

File "./Bug.v", line 7, characters 17-18:
Error: Syntax error: ',' or ')' expected after [term level 200] (in [term]).

$ rocq --version
The Rocq Prover, version 9.1.0
compiled with OCaml 4.14.2

The error is not reproduced in cases:

1. Search (?a !-> _ ; _).
2. double underscore is used Notation "'__' '!->' v" := (t_empty v) (at level 100, right associativity).

Small Rocq / Coq file to reproduce the bug

Definition total_map (A : Type) := nat -> A.
Definition t_empty {A : Type} (v : A) : total_map A := (fun _ => v).
Definition t_update {A : Type} (m : total_map A) (x : nat) (v : A) :=  fun x' => m x'.
Notation "'_' '!->' v" := (t_empty v) (at level 100, right associativity).
Notation "x '!->' v ';' m" := (t_update m x v) (at level 100, v at next level, right associativity).
Lemma t_update_eq : forall (A : Type) (m : total_map A) x v, (x !-> v ; m) x = v. Admitted.
Search (_ !-> _ ; _).

Version of Rocq / Coq where this bug occurs

9.1.0

Interface of Rocq / Coq where this bug occurs

No response

Last version of Rocq / Coq where the bug did not occur

No response

[SkySkimmer]

This is not particularly related to Search, it is just not possible to parse _ !-> _ ; _