coq - The formal proof system

Age	Commit message (Collapse)	Author
2021-04-08	remove `with hintdb` variant of Ltac2 `unify`, because	Samuel Gruetter
	passing one single hintdb is not quite the right API, we should pass a transparent state instead, but that would require an API for manipulating hintdbs and transparent states, postponing
2021-04-07	unify for Ltac2	Samuel Gruetter
	Fixes #14083
2021-03-24	Merge PR #13968: implement is_const, is_var, ... etc and has_evar for Ltac2	Pierre-Marie Pédrot
	Reviewed-by: ppedrot
2021-03-23	Merge PR #13914: Allow the presence of type casts for return values in Ltac2.	Michael Soegtrop
	Reviewed-by: MSoegtropIMC Reviewed-by: Zimmi48
2021-03-19	implement is_const, is_var, ... etc and has_evar for Ltac2	Samuel Gruetter
	Fixes #13963
2021-03-16	Slightly richer API allowing to shift the inductive in a block.	Pierre-Marie Pédrot

2021-03-16	Add tests for the new Ltac2 Ind API.	Pierre-Marie Pédrot

2021-03-10	Adding a parsing test.	Pierre-Marie Pédrot

2021-01-22	Add tests for the printf feature.	Pierre-Marie Pédrot

2020-11-30	Add test for this new function.	Pierre-Marie Pédrot

2020-07-06	Merge PR #11604: Primitive persistent arrays	Pierre-Marie Pédrot
	Ack-by: JasonGross Ack-by: SkySkimmer Ack-by: ejgallego Ack-by: gares Reviewed-by: ppedrot Ack-by: proux01 Ack-by: silene
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	Add a test for Ltac2 parsing of parameterized types.	Pierre-Marie Pédrot

2020-05-17	Ltac2: add notations for eval cbv in ... and other in place reductions	Michael Soegtrop

2020-05-11	More tests of rebinding Ltac2 definitions	Kenji Maillard

2020-05-11	Correcting ltac2's documentation on values turning test into proper check.	Kenji Maillard

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

2020-03-18	Adding a round-trip test for binders.	Pierre-Marie Pédrot

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-03	Ltac2: Add notation for enough and eenough	Michael Soegtrop

2020-02-08	Resolve #10342 : [Ltac2] Add array library	Michael Soegtrop

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

2019-06-25	Give a functional type to Ltac1 quotations with a context.	Pierre-Marie Pédrot
	This looks more principled, and doesn't require as much tinkering with the typing implementation.
2019-06-25	Adding the ability to transfer Ltac2 variables to Ltac1 quotations.	Pierre-Marie Pédrot

2019-06-06	[Ltac2] Interpretation scopes in “constr” arguments of tactic notations	Vincent Laporte

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.