coq - The formal proof system

Age	Commit message (Collapse)	Author
2021-04-19	Slightly tweak the not-unit Ltac2 warning.	Pierre-Marie Pédrot
	Fixes #11683.
2021-03-29	Print type of offending expression in Ltac2 not-unit warning.	Pierre-Marie Pédrot
	Partial fix of #14013.
2021-03-10	Allow to register deprecation status in Ltac2 term and notation declarations.	Pierre-Marie Pédrot

2020-11-04	Adding an if-then-else syntax to Ltac2.	Pierre-Marie Pédrot
	This is a syntactic sugar that is compiled away to a simple case analysis.
2020-05-11	Generalize the Ltac2 value criterion to pure let-bindings.	Pierre-Marie Pédrot

2020-05-11	Allow to rebind the old value of a mutable Ltac2 entry.	Pierre-Marie Pédrot

2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2019-10-29	Fix #10615: Notation substitution for Ltac2 terms.	Pierre-Marie Pédrot
	We implement a new type of "preterms" that represent untyped ASTs, corresponding to glob_expr in the ML implementations. Ltac2 quotations inside notations are provided with such preterms, and have to pretype them in order to do anything of relevance with them.
2019-10-18	Allow to pass Ltac1 values to Ltac2 quotations.	Pierre-Marie Pédrot
	This is the dual of #10344.
2019-06-17	Update headers of files that were stuck on older headers.	Théo Zimmermann
	Most of these files were introduced after #6543 but used older headers copied from somewhere else.
2019-06-08	Fix #10339: Anomaly in Ltac2.	Pierre-Marie Pédrot
	We use a user-facing wrapper instead of a low-level function raising internal exceptions.
2019-05-07	Integrate build and documentation of Ltac2	Maxime Dénès
	Since Ltac2 cannot be put under the stdlib logical root (some file names would clash), we move it to the `user-contrib` directory, to avoid adding another hardcoded path in `coqinit.ml`, following a suggestion by @ejgallego. Thanks to @Zimmi48 for the thorough documentation review and the numerous suggestions.