coq - The formal proof system

Age	Commit message (Collapse)	Author
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-19	Removed backtracking and default variants of various functions and added ↵	Michael Soegtrop
	option combinators
2019-06-18	Removed "b" from function names in Bool.v	Michael Soegtrop
	Changed year in headers
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?