coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-08-25	Propagate in-context information for extra arguments of notations too.	Hugo Herbelin

2020-02-22	New parsing/printing pattern/terms imp/scopes tests summarizing last changes.	Hugo Herbelin

2020-02-22	Propagate implicit arguments in all notations for partial applications.	Hugo Herbelin
	This was done for abbreviations but not string notations. This adopts the policy proposed in #11091 to make parsing and printing consistent.
2020-02-22	Deactivate implicit arguments in printing notations bound to "@f".	Hugo Herbelin
	This is to match the parsing policy (see #11091). In particular, we deactivate also argument scopes, consistently with what is done at parsing time.
2020-02-22	Fixing printing of notations bound to an expression of the form "@f".	Hugo Herbelin
	The CApp(CRef f,[]) encoding required to match the NApp(NRef f,[]) encoding of @f was lost. It remains to let printing match parsing wrt the deactivation of implicit arguments and argument scopes in such case. See next commit.
2020-02-22	Fixing a notation printing bug (missing a @ to reflect absence of imp. args).	Hugo Herbelin
	When a non-applied reference was matching a notation to the same reference, implicit arguments were lost.
2020-02-22	Fixing anomaly from #11091 (incompatible printing with notation and imp. args).	Hugo Herbelin
	We fix also an index error in deciding when to explicit print a non-inferable implicit argument.
2020-01-30	Printing tests for applied references combined with impl. args. and notations.	Hugo Herbelin
	This shows a few bugs and even anomalies. See issue #11091. See further commits for some fixes.