coq - The formal proof system

Age	Commit message (Expand)	Author
2017-08-01	Detyping functions are now operating on EConstr.t.	Pierre-Marie Pédrot
2017-08-01	Binding more primitive tactics.	Pierre-Marie Pédrot
2017-08-01	Fix typos. Improve wording.	Sam Pablo Kuper
2017-08-01	More in documentation.	Pierre-Marie Pédrot
2017-08-01	Improve style slightly	Sam Pablo Kuper
2017-08-01	Move glob_constr_ltac_closure to evar_refiner.	Maxime Dénès
2017-08-01	Merge PR #933: Fix documentation of Hint Mode (bug #4911).	Maxime Dénès
2017-08-01	Merge PR #932: Fix shuffled documentation.	Maxime Dénès
2017-08-01	Merge PR #929: Add missing paragraph to introduction	Maxime Dénès
2017-08-01	Merge PR #928: Fixing bug #5671 (tactic specialize unclean wrt Metas).	Maxime Dénès
2017-08-01	Merge PR #926: test-suite uses Extraction TestCompile	Maxime Dénès
2017-08-01	Merge PR #925: Document Extraction TestCompile	Maxime Dénès
2017-08-01	Merge PR #921: [make] remove compat5 file.	Maxime Dénès
2017-08-01	Merge PR #919: Remove a few useless evar-normalizations in printing code.	Maxime Dénès
2017-08-01	Merge PR #917: Moving --print-version to -print-version for consistency.	Maxime Dénès
2017-08-01	Merge PR #913: Less allocations in Detyping	Maxime Dénès
2017-08-01	Merge PR #909: Extraction: reduce primitive projections in types (fix bug 4709)	Maxime Dénès
2017-08-01	Merge PR #893: Removing default evar-normalization for ARGUMENT EXTEND.	Maxime Dénès
2017-08-01	Merge PR #834: Adding support for recursive notations of the form "x , .. , y...	Maxime Dénès
2017-08-01	Merge PR #806: closing bug 5315	Maxime Dénès
2017-08-01	Merge PR #775: [toplevel] Remove long ago deprecated and NOOP options.	Maxime Dénès
2017-08-01	adding a comment to explain the change	Julien Forest
2017-08-01	Fixup doc	Pierre-Marie Pédrot
2017-08-01	Fixup doc	Pierre-Marie Pédrot
2017-08-01	Adding documentation from the CEP.	Pierre-Marie Pédrot
2017-08-01	Do not thunk notations preemptively.	Pierre-Marie Pédrot
2017-08-01	Adding new scopes for standard Ltac structures.	Pierre-Marie Pédrot
2017-08-01	solving b1859	Julien Forest
2017-07-31	Fix incorrect use of "At the end".	Sam Pablo Kuper
2017-07-31	Minor grammar fix: replace a "then" with a "so".	Sam Pablo Kuper
2017-07-31	Replace jarring use of "Remark" with "Note"	Sam Pablo Kuper
2017-07-31	Update documentation of cumulativity	Amin Timany
2017-07-31	Improve errors for cumulativity when monomorphic	Amin Timany
2017-07-31	Change the option for cumulativity	Amin Timany
2017-07-31	Fix typo and Add Jason's example to the doc	Amin Timany
2017-07-31	Improve documentation of cumulativity	Amin Timany
2017-07-31	Add Jason's example of fun-ext with cumulativity	Amin Timany
2017-07-31	Add test for NonCumulative inductives	Amin Timany
2017-07-31	Issue error on monomorphic cumulative inductives	Amin Timany
2017-07-31	Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead	Maxime Dénès
2017-07-31	Merge PR #746: Timing on ci via coq_makefile for various projects	Maxime Dénès
2017-07-31	[general] Remove spurious dependency of highparsing on toplevel.	Emilio Jesus Gallego Arias
2017-07-31	better `try with` scope in `discr_positions`	amblaf
2017-07-31	Correcting [build_discriminator] to make the test-suite pass	amblaf
2017-07-31	Replacing tclENV with the goal environment	amblaf
2017-07-31	env, sigma as first arguments of functions	amblaf
2017-07-31	Remove references to Global.env in tactics/*.ml	amblaf
2017-07-30	Exporting more internals from Coq implementation.	Pierre-Marie Pédrot
2017-07-29	Drop paragraph mentioning Addendum as separate doc.	Théo Zimmermann
2017-07-29	closing bug 5315	Julien Forest