coq - The formal proof system

Age	Commit message (Expand)	Author
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
2017-07-28	Parameterizing FFI functions for parameterized types.	Pierre-Marie Pédrot
2017-07-28	Moving the Ltac2 FFI to a separate file.	Pierre-Marie Pédrot
2017-07-28	Merge PR #923: [api] Fix base_include LTAC parts.	Maxime Dénès
2017-07-28	Merge PR #889: Removing template polymorphism for definitions.	Maxime Dénès
2017-07-28	Merge PR #888: Stronger kernel types	Maxime Dénès
2017-07-28	Merge PR #823: Async off in Windows by default in CoqIDE	Maxime Dénès
2017-07-28	Merge PR #782: Update API for fiat	Maxime Dénès
2017-07-28	Allowing generic patterns in let-bindings.	Pierre-Marie Pédrot
2017-07-28	Fix some coq-tex errors in the reference manual.	Guillaume Melquiond
2017-07-28	Fix documentation of Hint Mode (bug #4911).	Guillaume Melquiond
2017-07-28	Fix shuffled documentation.	Guillaume Melquiond
2017-07-28	Merge PR #852: Makefile: fails if some .vo or .cm* file has no source	Maxime Dénès
2017-07-27	Add missing paragraph to introduction	Benjamin Pierce
2017-07-27	Fixing bug #5671 (specialize unclean wrt Metas).	Hugo Herbelin
2017-07-27	Factorizing code for constructors and tuples.	Pierre-Marie Pédrot
2017-07-27	Extraction.tex: mention the possible "From Coq Require Extraction"	letouzey
2017-07-27	Cleaning up code in internalization.	Pierre-Marie Pédrot