coq - The formal proof system

Age	Commit message (Collapse)	Author
2019-05-10	Use Print Custom Grammar to inspect custom entries	Jasper Hugunin

2019-04-29	Revert #8187	Vincent Laporte

2019-04-29	Revert #9249	Vincent Laporte

2019-02-19	Notations: Fixing a printing bug with patterns.	Hugo Herbelin
	Parameters had to be removed in cases_pattern_of_glob_constr.
2019-02-04	Primitive integers	Maxime Dénès
	This work makes it possible to take advantage of a compact representation for integers in the entire system, as opposed to only in some reduction machines. It is useful for heavily computational applications, where even constructing terms is not possible without such a representation. Concretely, it replaces part of the retroknowledge machinery with a primitive construction for integers in terms, and introduces a kind of FFI which maps constants to operators (on integers). Properties of these operators are expressed as explicit axioms, whereas they were hidden in the retroknowledge-based approach. This has been presented at the Coq workshop and some Coq Working Groups, and has been used by various groups for STM trace checking, computational analysis, etc. Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr> Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr> Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
2019-01-25	Notations: Removing useless parentheses on abbrevs for prefix of an application.	Hugo Herbelin

2018-12-25	Fixing printing bug due to using equality ill-checking hash key of kernel name.	Hugo Herbelin
	Thanks to Georges Gonthier for noticing it. Expanding a few Pervasives.compare at this occasion.
2018-12-04	Giving to type_scope a softer role in printing.	Hugo Herbelin
	Namely, it does not explicitly open a scope, but we remember that we don't need the %type delimiter when in type position.
2018-12-04	Printing priority to most recent notation in case of non-open scopes with delim.	Hugo Herbelin
	This modifies the strategy in previous commits so that priorities are as before in case of non-open scopes with delimiters. Additionally, we document the rare situation of overlapping applicative notations (maybe this is too rare and ad hoc to be worth being documented though).
2018-12-04	Using scope for printing: more tests.	Hugo Herbelin

2018-12-04	Fixing #8551 (missing delimiters when notation exists both lonely and in scope).	Hugo Herbelin

2018-12-04	Selecting which notation to print based on current stack of scope.	Hugo Herbelin
	See discussion on coq-club starting on 23 August 2016.
2018-11-20	Notations: Trying using a notation with or w/o removal of coercions.	Hugo Herbelin
	Preferring a notation which does require a delimiter, depending on whether the coercion is removed or not, was done for primitive tokens. We do it for all notations.
2018-10-31	Notations: fixing a bug with abbreviations in custom entries.	Hugo Herbelin
	Coercions were missing.
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.