coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-11-15	Ensuring the body of the notation in Locate is printed at level 0.	Hugo Herbelin
	This is consistent with the syntax of Notation and is (IMO) clearer.
2020-11-15	Adding support for Locate "( x , y )".	Hugo Herbelin
	It finds "( x , y , .. , z )". Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-11-15	Fixing Locate for recursive notations with names.	Hugo Herbelin
	E.g. Locate "(x , y , .. , z )" now works while only Locate "(_ , _ , .. , _ )" was working before. This also fixes a confusion between a variable and its anonymization into _, wrongly finding notations mentioning '_'. Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-10-10	New spacing/formatting in Locate Notation, Print Scopes, Print Visibility.	Hugo Herbelin

2019-10-17	Fix Locate printing regression	Guillaume Melquiond
	Fixes #9428. (Again.) This is a cherry-pick of 68927ac4/4b02fbd9 bugfixes, because 0251c800 reverted them. Corrects a 8.9.1 → 8.10.0 regression. (cherry picked from commit 68927ac48b1ce8fe30edef24defdcdc84173a5a5)