coq - The formal proof system

Age	Commit message (Expand)	Author
2017-08-02	Makefile: 'make clean' now immune to the check for binary files without sources	Pierre Letouzey
2017-08-02	Typo in the documentation of cumulativity	Amin Timany
2017-08-01	Unbreak RecTutorial.v	Gaëtan Gilbert
2017-08-01	Remove old doc/rt files.	Gaëtan Gilbert
2017-08-01	Add dev/v8-syntax/check-grammar byproducts to gitignore.	Gaëtan Gilbert
2017-08-01	Remove obsolete files	Gaëtan Gilbert
2017-08-01	Add .v extension to dev/doc/notes-on-conversion	Gaëtan Gilbert
2017-08-01	Remove dev/TODO	Gaëtan Gilbert
2017-08-01	Fix syntax-v8.tex bad parenthesizing	Gaëtan Gilbert
2017-08-01	Remove unused Makefiles in dev/tools/	Gaëtan Gilbert
2017-08-01	[flags] Remove XML output flag.	Emilio Jesus Gallego Arias
2017-08-01	Remove understand_tcc_evars.	Maxime Dénès
2017-08-01	Move type_uconstr to Tacinterp.	Maxime Dénès
2017-08-01	Have coq-dpdgraph ci test print the differences	Jason Gross
2017-08-01	Remove understand_judgment and understand_judgment_tcc.	Maxime Dénès
2017-08-01	Remove allow_anonymous_refs.	Maxime Dénès
2017-08-01	Remove pure_open_constr (now open_constr)	Maxime Dénès
2017-08-01	Printing goals does not evar-normalizes beforehand anymore.	Pierre-Marie Pédrot
2017-08-01	Detyping functions are now operating on EConstr.t.	Pierre-Marie Pédrot
2017-08-01	Fix typos. Improve wording.	Sam Pablo Kuper
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	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