aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-03-07Adding backtraces to scheme error messages.Pierre-Marie Pédrot
2016-03-07Re-enable OCaml warnings disabled by mistake as part of e759333.Maxime Dénès
2016-03-05Fixing bug #4608: Anomaly "output_value: abstract value (outside heap)".Pierre-Marie Pédrot
2016-03-04Fix #4607: do not read native code files if native compiler was disabled.Maxime Dénès
2016-03-04This fix is probably not enough to justify that there are no problems withMaxime Dénès
2016-03-04Rename Ephemeron -> CEphemeron.Maxime Dénès
2016-03-04Fix a typo in dev/doc/changes.txtJason Gross
2016-03-03Adding a test for the behaviour of open_constr described in #3777.Pierre-Marie Pédrot
2016-03-03Fixing bug #4105: poor escaping in the protocol between CoqIDE and coqtop.Pierre-Marie Pédrot
2016-02-28Fixing bug #4596: [rewrite] broke in the past few weeks.Pierre-Marie Pédrot
2016-02-24Document Hint Mode, cleanup Hint doc.Matthieu Sozeau
2016-02-23Document differences of Hint Resolve and Hint ExternMatthieu Sozeau
2016-02-23Fix part of bug #4533: respect declared global transparency ofMatthieu Sozeau
2016-02-23Fix bug #4544: Backtrack on using full betaiota reduction during keyed unific...Matthieu Sozeau
2016-02-20Fixing bug #4540: CoqIDE bottom progress bar does not update.Pierre-Marie Pédrot
2016-02-19Fix regression from 8.4 in reflexivity/...Matthieu Sozeau
2016-02-19Fixing bug #4580: [Set Refine Instance Mode] also used for Program Instance.Pierre-Marie Pédrot
2016-02-19Fixing bug #4582: cannot override notation [ x ].Pierre-Marie Pédrot
2016-02-19STM: Print/Extraction have to be skipped if -quickEnrico Tassi
2016-02-19CoqIDE: STOP button also stops workers (fix #4542)Enrico Tassi
2016-02-19STM: classify some variants of Instance as regular `Fork nodes.Enrico Tassi
2016-02-17Fixing the Proofview.Goal.goal function.Pierre-Marie Pédrot
2016-02-17Fix bug #4574: Anomaly: Uncaught exception Invalid_argument("splay_arity").Pierre-Marie Pédrot
2016-02-13Do not give a name to anonymous evars anymore. See bug #4547.Pierre-Marie Pédrot
2016-02-10STM: always stock in vio files the first node (state) of a proofEnrico Tassi
2016-02-10STM: not delegate proofs that contain Vernac(Module|Require|Import), #4530Enrico Tassi
2016-02-10Don't fail fatally if PATH is not set.Emilio Jesus Gallego Arias
2016-02-08Improving error message with missing patterns in the presence ofHugo Herbelin
2016-02-03Optimizing the universes_of_constr_function.Pierre-Marie Pédrot
2016-02-03Optimizing the computation of frozen evars.Pierre-Marie Pédrot
2016-02-03Opacifying the type of evar naming structure in Evd.Pierre-Marie Pédrot
2016-02-03More compact representation for evar resolvability flag.Pierre-Marie Pédrot
2016-01-27Fix bug #4537: Coq 8.5 is slower in typeclass resolution.Pierre-Marie Pédrot
2016-01-26Fixing bde12b70 about reporting ill-formed constructor.Hugo Herbelin
2016-01-24Tentative fix for bug #4522: Incorrect "Warning..." on windows.Pierre-Marie Pédrot
2016-01-24Fixing bug #4373: coqdep does not know about .vio files.Pierre-Marie Pédrot
2016-01-24Fixing bug #3826: "Incompatible module types" is uninformative.Pierre-Marie Pédrot
2016-01-24Adding a test for bug #4378.Pierre-Marie Pédrot
2016-01-24Fixing bug #4495: Failed assertion in metasyntax.ml.Pierre-Marie Pédrot
2016-01-24Fixing bug #4511: evar tactic can create non-typed evars.Pierre-Marie Pédrot
2016-01-23Fix bug #4503: mixing universe polymorphic and monomorphicMatthieu Sozeau
2016-01-23Fix bug #4519: oops, global shadowed local universe level bindings.Matthieu Sozeau
2016-01-23Implement support for universe binder lists in Instance and Program Fixpoint/...Matthieu Sozeau
2016-01-23Fix bug #4506. Using betadeltaiota_nolet might produce terms of the formMatthieu Sozeau
2016-01-22Restore warnings produced by the interpretation of the command lineHugo Herbelin
2016-01-21Compile OS X binaries without native_compute support.Maxime Dénès
2016-01-20Update cic.mli MD5 after header update.Maxime Dénès
2016-01-20Update version number in configure.Maxime Dénès
2016-01-20Update copyright headers.Maxime Dénès
2016-01-20Change $(...)$ to ltac:(...) in section 2.11. Fixes #4500.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 08:29:12 +0000