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
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
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-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-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.