coq - The formal proof system

Age	Commit message (Collapse)	Author
2021-04-07	[abbreviation] allow the user to set arguments scope	Enrico Tassi

2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2020-03-04	Adding support for an "only parsing" modifier in "where"-based notations.	Hugo Herbelin
	Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
2019-12-02	Remove deprecated compat modifier of Notation / Infix commands.	Théo Zimmermann
	And simplify a lot the compatibility infrastructure following this. Update dev/tools/update-compat.py Remove much complexity. Co-authored-by: Jason Gross <jgross@mit.edu>
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann

2019-06-06	`deprecated` attribute support for notations and syntactic definitions	Maxime Dénès
	We also slightly change the semantics of the `compat` syntax modifier to re-express it in terms of the `deprecated` attribute, and we deprecate it in favor of the latter.
2019-05-10	Use Print Custom Grammar to inspect custom entries	Jasper Hugunin

2018-09-10	Support for Local flag in Declare Scope, Undelimit/Delimit Scope, Bind Scope.	Hugo Herbelin
	This is for use in modules. By default, the behavior is local in sections and Global is forbidden in sections. By default, the behavior is global in modules.
2018-09-10	Adding a command "Declare Scope" and deprecating scope implicit declaration.	Hugo Herbelin

2018-07-29	Supporting locality flag for custom entries + compatibility with modules.	Hugo Herbelin
	Also prevents to use an entry name already defined.
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-06-12	[api] Misctypes removal: miscellaneous aliases.	Emilio Jesus Gallego Arias

2018-02-27	Update headers following #6543.	Théo Zimmermann

2018-02-22	[ast] Improve precision of Ast location recognition in serialization.	Emilio Jesus Gallego Arias
	We follow the suggestions in #402 and turn uses of `Loc.located` in `vernac` into `CAst.t`. The impact should be low as this change mostly affects top-level vernaculars. With this change, we are even closer to automatically map a text document to its AST in a programmatic way.
2018-02-20	Moving Metasyntax.register_grammar to Pcoq for usability in Egramcoq.	Hugo Herbelin
	Renaming it register_grammars_by_name.
2018-02-17	Change references to CAMLP4 to CAMLP5 to be more accurate since we no	Jim Fehrle
	longer use camlp4.
2017-10-05	Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.).	Hugo Herbelin
	This allows e.g. the following to work: Reserved Notation "* a" (at level 70). Inductive P {n : nat} : nat -> Prop := c m : m where " m" := (P m). We seize this opportunity to make main calls to Metasyntax to depend on an arbitrary env rather than on Global.env. Incidentally, this fixes a little coqdoc bug in classifying the inductive type referred to in the "where" clause.
2017-07-27	deprecate Pp.std_ppcmds type alias	Matej Košík

2017-07-04	Bump year in headers.	Pierre-Marie Pédrot

2017-02-15	[stm] Break stm/toplevel dependency loop.	Emilio Jesus Gallego Arias
	Currently, the STM, vernac interpretation, and the toplevel are intertwined in a mutual dependency that needs to be resolved using imperative callbacks. This is problematic for a few reasons, in particular it makes the interpretation of commands that affect the document quite intricate. As a first step, we split the `toplevel/` directory into two: "pure" vernac interpretation is moved to the `vernac/` directory, on which the STM relies. Test suite passes, and only one command seems to be disabled with this approach, "Show Script" which is to my understanding obsolete. Subsequent commits will fix this and refine some of the invariants that are not needed anymore.