coq - The formal proof system

Age	Commit message (Collapse)	Author
2019-05-14	Merge PR #10125: Allow run_tactic to return a value, remove hack from ltac2	Pierre-Marie Pédrot
	Ack-by: SkySkimmer Reviewed-by: ppedrot
2019-05-14	Merge PR #10136: [ltac2] Add primitive integers	Pierre-Marie Pédrot
	Ack-by: SkySkimmer Reviewed-by: ppedrot
2019-05-14	Allow run_tactic to return a value, remove hack from ltac2	Gaëtan Gilbert

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

2019-05-10	Make the check flag of conversion functions mandatory.	Pierre-Marie Pédrot
	The current situation is a mess, some functions set it by default, but other no. Making it mandatory ensures that the expected value is the correct one.
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.