coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-07-03	Fix #11121: Simultaneous definition of term and notation in custom grammar	Maxime Dénès

2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2020-02-22	Merge PR #11635: Cleanup around the tolerability structure	Emilio Jesus Gallego Arias
	Reviewed-by: ejgallego
2020-02-22	Making structure of type "tolerability" and related clearer.	Hugo Herbelin
	Also renamed it to relative_entry_level. Correspondence between old and new representation is: (n,L) -> LevelLt n (n,E), (n,Prec n) -> LevelLe n (n,Any) -> LevelSome (n,Prec p) when n<>p was unused Should not change global semantics (except error message in pr_arg).
2020-02-21	Notations: Avoiding computing parsing rule when in onlyprinting mode.	Hugo Herbelin
	In particular, this fixes #9741.
2020-02-19	Addressing #6082 and #7766 (overriding format of notation).	Hugo Herbelin
	We do two changes: - We distinguish between a notion of format generically attached to notations and a new notion of format attached to interpreted notations. "Reserved Notation" attaches a format generically. "Notation" attaches the format specifically to the given interpretation, and additionally, attaches it generically if it is the first time the notation is defined. - We warn before overriding an explicitly reserved generic format, or a specific format.
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann

2018-05-31	[notations] Split interpretation and parsing of notations	Emilio Jesus Gallego Arias
	Previously to this patch, `Notation_term` contained information about both parsing and notation interpretation. We split notation grammar to a file `parsing/notation_gram` as to make `interp/` not to depend on some parsing structures such as entries.