aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-07-06Merge branch 'v8.5' into trunkMaxime Dénès
2015-07-06Temporarily disable test file for #3922.Maxime Dénès
2015-07-06Test case for #4203, fixed by commit a51cce36.Maxime Dénès
2015-07-05Fixing documentation (see Maxime's mail on coqdev, July 3).Hugo Herbelin
2015-07-05More precise rewording about asymmetric patterns.Hugo Herbelin
2015-07-05Fix handling of primitive projections in VM.Maxime Dénès
2015-07-03Fixing bug #4265: coqdep does not handle From ... Require.Pierre-Marie Pédrot
2015-07-03Fix convertibility of primitive projections for native_compute.Maxime Dénès
2015-07-02Remove a line from test-suite.Maxime Dénès
2015-07-02Merge branch 'v8.5' into trunkMaxime Dénès
2015-07-02More robust pattern matching on structured constants in VM.Maxime Dénès
2015-07-02Revert "Add target to install dev files."Maxime Dénès
2015-07-02Fix loop in assumptions (Close: #4275)Enrico Tassi
2015-07-02Display functions for primitive projections.Maxime Dénès
2015-07-01Further simplification of the graph traversal in Univ.Pierre-Marie Pédrot
2015-07-01Notation: use same level for "@" in constr: and pattern: (Close: #4272)Enrico Tassi
2015-06-30Removing dead code in coqdep.Pierre-Marie Pédrot
2015-06-30Another missing Fail and comment in test-suite.Maxime Dénès
2015-06-30Missing "Fail" in test-suite.Maxime Dénès
2015-06-29Assumptions: more informative print for False axiom (Close: #4054)Enrico Tassi
2015-06-29class_tactics: make interruptibleEnrico Tassi
2015-06-29class_tactics: remove catch-all, use Errors.noncriticalEnrico Tassi
2015-06-29win: compile with -debugEnrico Tassi
2015-06-29Fix test file for #4214 which was fixed by Hugo.Maxime Dénès
2015-06-29Better test case by PMP for #3948.Maxime Dénès
2015-06-29Code documentation of the TACTIC/VERNAC EXTEND macros.Pierre-Marie Pédrot
2015-06-28Merge branch 'v8.5'Pierre-Marie Pédrot
2015-06-28Fix incompleteness of conversion used by evarconvMatthieu Sozeau
2015-06-28Reinstall Set Printing Universes option overwritten by Maxime!Matthieu Sozeau
2015-06-26Share prop/set values in sorts.ml.Matthieu Sozeau
2015-06-26Fix bug #4254 with the help of J.H. JourdanMatthieu Sozeau
2015-06-26BUGFIX: Three fixes for the price of 1 in sorts.ml:Matthieu Sozeau
2015-06-26Add target to install dev files.Matthieu Sozeau
2015-06-26Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"Lionel Rieg
2015-06-26Typos in my previous edition of the reference manual.Assia Mahboubi
2015-06-26Some edition in the coq_makefile/_CoqProject section.Assia Mahboubi
2015-06-26Added _CoqProject to the index of the reference manual.Assia Mahboubi
2015-06-25Adding a more efficient representation of OCaml objects in votour.Pierre-Marie Pédrot
2015-06-25Remove other types not carried by interpretations in `Tacexpr`.Arnaud Spiwack
2015-06-25Remove useless `and_short_name` in interpreted level in `Tacexpr`.Arnaud Spiwack
2015-06-25Wrapped the declare_object function to pretty-print anomalies at loading time.Thomas Sibut-Pinote
2015-06-25Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Thomas Sibut-Pinote
2015-06-24Extend test-suite for the positivity checker.Arnaud Spiwack
2015-06-24More silent Makefile when looking for codesign.Maxime Dénès
2015-06-24Fix test-suite after 1343b69221ce3eeb3154732e73bbdc0044b224a8.Maxime Dénès
2015-06-24Less closures makes the GC happy.Pierre-Marie Pédrot
2015-06-24Merge branch 'v8.5'Pierre-Marie Pédrot
2015-06-24Add a space in cast since cast binds loosely.Gregory Malecha
2015-06-24improve --help documentation: the -m|--memory option was missingGabriel Scherer
2015-06-24when OCAML_GC_STATS points to a filepath, write Gc stats into itGabriel Scherer
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-18 20:03:10 +0000