aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-08-16Merge PR #864: Some cleanups after cumulativity for inductive typesMaxime Dénès
2017-08-15Removing trailing "/" and "\" in directory names only on win32.Hugo Herbelin
2017-08-15Adding a test for BZ#1859 as suggested by @tchajed.Théo Zimmermann
2017-08-13Makefile : ignore user-contrib in various file searchesPierre Letouzey
2017-08-12Moving file primitive.ml to cPrimitive.ml to avoid conflict with OCaml.Hugo Herbelin
2017-08-12Merge PR #963: fix coq_makefileMaxime Dénès
2017-08-12fix coq_makefileMatej Košík
2017-08-12More portable location for the time command.Théo Zimmermann
2017-08-08Set detachable windows type hint to dialog.Olivier Marty
2017-08-06Print names of all open blocksTej Chajed
2017-08-04Makefile: install-byte works even if -coqide noEnrico Tassi
2017-08-03Amend wording to capture intended meaningSam Pablo Kuper
2017-08-02Rewording the introductionEnrico Tassi
2017-08-02Rephrasing a couple of sentences in a more factual way.Hugo Herbelin
2017-08-02Rephrasing the introduction in a more factual and up-to-date way.Hugo Herbelin
2017-08-02Port ssr manual to Coq's latex/hevea styleEnrico Tassi
2017-08-02Makefile.doc: implement serve-refman-8080 targetEnrico Tassi
2017-08-02Update Setoid.texlarsr
2017-08-02Makefile: 'make clean' now immune to the check for binary files without sourcesPierre Letouzey
2017-08-02Typo in the documentation of cumulativityAmin Timany
2017-08-01Unbreak RecTutorial.vGaëtan Gilbert
2017-08-01Remove old doc/rt files.Gaëtan Gilbert
2017-08-01Add dev/v8-syntax/check-grammar byproducts to gitignore.Gaëtan Gilbert
2017-08-01Remove obsolete filesGaëtan Gilbert
2017-08-01Add .v extension to dev/doc/notes-on-conversionGaëtan Gilbert
2017-08-01Remove dev/TODOGaëtan Gilbert
2017-08-01Fix syntax-v8.tex bad parenthesizingGaëtan Gilbert
2017-08-01Remove unused Makefiles in dev/tools/Gaëtan Gilbert
2017-08-01[flags] Remove XML output flag.Emilio Jesus Gallego Arias
2017-08-01Have coq-dpdgraph ci test print the differencesJason Gross
2017-08-01Printing goals does not evar-normalizes beforehand anymore.Pierre-Marie Pédrot
2017-08-01Detyping functions are now operating on EConstr.t.Pierre-Marie Pédrot
2017-08-01Fix typos. Improve wording.Sam Pablo Kuper
2017-08-01Improve style slightlySam Pablo Kuper
2017-08-01Merge PR #933: Fix documentation of Hint Mode (bug #4911).Maxime Dénès
2017-08-01Merge PR #932: Fix shuffled documentation.Maxime Dénès
2017-08-01Merge PR #929: Add missing paragraph to introductionMaxime Dénès
2017-08-01Merge PR #928: Fixing bug #5671 (tactic specialize unclean wrt Metas).Maxime Dénès
2017-08-01Merge PR #926: test-suite uses Extraction TestCompileMaxime Dénès
2017-08-01Merge PR #925: Document Extraction TestCompileMaxime Dénès
2017-08-01Merge PR #921: [make] remove compat5 file.Maxime Dénès
2017-08-01Merge PR #919: Remove a few useless evar-normalizations in printing code.Maxime Dénès
2017-08-01Merge PR #917: Moving --print-version to -print-version for consistency.Maxime Dénès
2017-08-01Merge PR #913: Less allocations in DetypingMaxime Dénès
2017-08-01Merge PR #909: Extraction: reduce primitive projections in types (fix bug 4709)Maxime Dénès
2017-08-01Merge PR #893: Removing default evar-normalization for ARGUMENT EXTEND.Maxime Dénès
2017-08-01Merge PR #834: Adding support for recursive notations of the form "x , .. , y...Maxime Dénès
2017-08-01Merge PR #806: closing bug 5315Maxime Dénès
2017-08-01Merge PR #775: [toplevel] Remove long ago deprecated and NOOP options.Maxime Dénès
2017-08-01adding a comment to explain the changeJulien Forest
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 17:35:10 +0000