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-20	Merge PR #10832: Addressing #6082 and #7766: warning when overriding ↵	Emilio Jesus Gallego Arias
	notation format + new notion of format associated to a given interpretation Ack-by: maximedenes
2020-02-19	Revert "Granting #9516 and #9518 (support for numerals and strings in custom ↵	Hugo Herbelin
	entries)." This reverts commit 29919b725262dca76708192bde65ce82860747be. It was pushed by mistake as part of #11530. Sorry about it.
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.
2020-02-16	Revert "Suite picking numeral notation"	Hugo Herbelin
	This reverts commit 03c48bb6943312e606b80b7af65b1ccb7122a386.
2020-02-16	Suite picking numeral notation	Hugo Herbelin
	Ceci est une suite à numeral notation in custom entries, cherchant à raffiner la compatibilité entre entrées. C'est mélangé avec le "pick" précédent, et c'est en chantier.
2020-02-16	Granting #9516 and #9518 (support for numerals and strings in custom entries).	Hugo Herbelin

2020-02-15	Reorganize type "production_level" along a more intuitive structure.	Hugo Herbelin
	NextLevel = at next level NumLevel n = at level n DefaultLevel = <no mention of level>
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann

2018-09-02	Fixing #8106 (anomaly if declaring levels for only printing then only parsing).	Hugo Herbelin
	Notations were not initially designed to support independent parsing and printing rules. Some redesign of this part of the code shall be necessary at some time.
2018-07-29	Renaming ETName and ETReference so as to fit the user-visible terminology.	Hugo Herbelin
	ETName -> ETIdent ETReference -> ETGlobal
2018-07-29	Adding support for custom entries in notations.	Hugo Herbelin
	- New command "Declare Custom Entry bar". - Entries can have levels. - Printing is done using a notion of coercion between grammar entries. This typically corresponds to rules of the form 'Notation "[ x ]" := x (x custom myconstr).' but also 'Notation "{ x }" := x (in custom myconstr, x constr).'. - Rules declaring idents such as 'Notation "x" := x (in custom myconstr, x ident).' are natively recognized. - Rules declaring globals such as 'Notation "x" := x (in custom myconstr, x global).' are natively recognized. Incidentally merging ETConstr and ETConstrAsBinder. Noticed in passing that parsing binder as custom was not done as in constr. Probably some fine-tuning still to do (priority of notations, interactions between scopes and entries, ...). To be tested live further.
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.