aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-07-10Continuing handling of NoCoercion after df6e64fd28 and 4944b5e72.Hugo Herbelin
2015-07-10Option -type-in-type: added support in checker and making it contaminatingHugo Herbelin
2015-07-10Highlighting Universe in CoqIDE.Hugo Herbelin
2015-07-10CHANGES: grammatical correction, suggested by Jason Gross on Bugzilla.Maxime Dénès
2015-07-10Native compiler: make non-fatal linking errors silent except in debug mode.Maxime Dénès
2015-07-10Native compiler: refactor code handling pre-computed values.Maxime Dénès
2015-07-09Kernel/Checker: Cleanup fixes of substitutions due to let-ins.Matthieu Sozeau
2015-07-09Kernel: primitive projections handling of let-insMatthieu Sozeau
2015-07-09Improve semantics of -native-compiler flag.Maxime Dénès
2015-07-09Template polymorphism: A bug-fix for Bug #4258mlasson
2015-07-09Make retyping of projections more resilient to wrong environment.Maxime Dénès
2015-07-09Fixing printing of primitive coinductive record status.Pierre-Marie Pédrot
2015-07-08Ide: fix bug #4284 for goodMatthieu Sozeau
2015-07-08Bug 4284: Tentative bugfix for detyping exception.Matthieu Sozeau
2015-07-08Checker: Report bugfixes from kernel/inductive.mlMatthieu Sozeau
2015-07-08Fix documentation of universes.Matthieu Sozeau
2015-07-08Make sure that scope classes are displayed by Print Scopes. (Fix bug #4262)Guillaume Melquiond
2015-07-08Fix command-line documentation of coq-tex.Guillaume Melquiond
2015-07-08Fix documentation.Guillaume Melquiond
2015-07-08Use the same optimization level for the VM, whatever the debug level.Guillaume Melquiond
2015-07-07Document Set/Print Firstorder Solver option.Matthieu Sozeau
2015-07-07Checker: Fix bug #4282Matthieu Sozeau
2015-07-07Univs: bug fix.Matthieu Sozeau
2015-07-07test-suite: Fix test-suite MakefileMatthieu Sozeau
2015-07-07Univs/minimization: Fix unused variable bug.Matthieu Sozeau
2015-07-07Fixing "Load" without "Verbose" in coqtop, after vernac_com lost itsHugo Herbelin
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-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-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-29Code documentation of the TACTIC/VERNAC EXTEND macros.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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-28 00:35:28 +0000