coq - The formal proof system

Age	Commit message (Collapse)	Author
2021-03-19	implement is_const, is_var, ... etc and has_evar for Ltac2	Samuel Gruetter
	Fixes #13963
2021-01-04	Remove redundant univ and parameter info from CaseInvert	Gaëtan Gilbert

2020-07-06	Primitive persistent arrays	Maxime Dénès
	Persistent arrays expose a functional interface but are implemented using an imperative data structure. The OCaml implementation is based on Jean-Christophe Filliâtre's. Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr> Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-07-01	UIP in SProp	Gaëtan Gilbert

2020-03-18	Actually use the binder type for Ltac2 that should be used in the kernel.	Pierre-Marie Pédrot
	That is, it contains the type of the binder so as not to rely on the relevance explicitly.
2020-03-18	Hide the Ltac2 binder type.	Pierre-Marie Pédrot
	For robustness and it is better to leave it opaque. Users are not supposed to fiddle with it.
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2019-11-01	Add primitive floats to Ltac2	Pierre Roux

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-09-24	Fix #10783: use binder_annot in Ltac2.Constr.Unsafe.kind	Gaëtan Gilbert

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-05-23	Fixing typos - Part 2	JPR

2019-05-10	[ltac2] Add primitive integers	Pierre Roux

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.