coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-11-20	Add preliminary support for notations with large class (non-recursive) binders.	Hugo Herbelin
	We introduce a class of open binders which includes "x", "x:t", "'pat" and a class of closed binders which includes "x", "(x:t)", "'pat".
2020-10-08	Dropping the misleading int argument of Pp.h.	Hugo Herbelin
	An h-box inhibits the breaking semantics of any cut/spc/brk in the enclosed box. We tentatively replace its occurrence by an h or hv, assuming in particular that if the indentation is not 0, an hv box was intended.
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-23	Cancelling precedences in Set Printing Parentheses only at border of notations.	Hugo Herbelin

2020-02-22	Simplification of type unparsing (index of variable in UnpMetaVar is unused).	Hugo Herbelin

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-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-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.