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-22	Add a type of format strings to Ltac2.	Pierre-Marie Pédrot
	It provides an abstract type of well-typed format strings, a scope to parse them and a minimal printf-like API.
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-10-07	chmod -x some files	Jason Gross
	They probably don't need to be executable
2019-06-25	Merge PR #10219: [Ltac2] Add util files for Bool, List, Option	Pierre-Marie Pédrot
	Ack-by: JasonGross Ack-by: MSoegtropIMC Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: ppedrot
2019-06-19	Removed backtracking and default variants of various functions and added ↵	Michael Soegtrop
	option combinators
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-16	- added OCaml copyright header to List.v (if for no other reason than out of ↵	Michael Soegtrop
	courtesy) - index errors (negative or out of bounds) generally throw (panic) - hd, last, find backtrack, because here backtracking can actually be useful added a _throw variant to these functions which panics This emaphasizes the difference between backtracking and throwing exceptions, which doesn't exist in OCaml. - simplified the implementation of for_all2 and exist2 (ok, that is a matter of taste ...) - added assertions which combine a boolean match with a throw. This makes the code more readable and makes it easier to have more specific error messages. - added a lastn function - gave Out_of_bounds a message argument (there is no good reason why invalid_argument has one and this not) All other exceptions without message argument are quite specific to certain functions (like Not_Found)
2019-05-22	[Ltac2] Add util files for Bool, List, Option	Jason Gross
	Most functions are taken either from the Coq standard library or the OCaml standard library. One (`enumerate`) is taken from Python. Most names are chosen according to OCaml conventions (as Coq does not have exceptions, and so the OCaml naming conventions already distinguish between option and exception). Since `exists` is a keyword, we use the Coq name `existsb` instead. We generally favor Coq argument ordering when there is a conflict between Coq and OCaml. Note that `seq` matches neither Coq nor OCaml; it takes a `step` argument for how much to increment by on each step. Sorting functions are mostly taken from Coq's mergesort library; it might make sense to replace them with OCaml's versions for efficiency?
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.