aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2016-01-20Documenting Set Bullet Behavior.Hugo Herbelin
2016-01-20Clarifying the documentation of tactics "cbv" and "lazy".Hugo Herbelin
2016-01-20Fixing Not_found on unknown bullet behavior.Hugo Herbelin
2016-01-19Fix bug #4420: check_types was losing universe constraints.Matthieu Sozeau
2016-01-15Thanks Hugo, but let's remain factual.Maxime Dénès
2016-01-15Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Maxime Dénès
2016-01-15Minor edits in output of coqdep --help.Maxime Dénès
2016-01-15Fix #4408.Pierre Courtieu
2016-01-15Partially fixing #4408: coqdep --help is up to date.Pierre Courtieu
2016-01-13MMaps: remove it from final 8.5 release, since this new library isn't mature ...Pierre Letouzey
2016-01-13Fixing success of test for #3848 after move to directory "closed".Hugo Herbelin
2016-01-13Fixing #4467 (continued).Hugo Herbelin
2016-01-12Fixing #4467 (missing shadowing of variables in cases pattern).Hugo Herbelin
2016-01-12Fixing #4256 and #4484 (changes in evar-evar resolution made that newHugo Herbelin
2016-01-12Reporting about the new tactical unshelve.Hugo Herbelin
2016-01-12Extend last commit: keyed unification uses full conversions on the applied co...Matthieu Sozeau
2016-01-12Extend Keyed Unification tests with the one from R. Krebbers.Matthieu Sozeau
2016-01-12Fix essential bug in new Keyed Unification mode reported by R. Krebbers.Matthieu Sozeau
2016-01-12Referring to coq.inria.fr/stdlib for more on libraries and ltac-level tactics.Hugo Herbelin
2016-01-12Documenting dtauto and dintuition.Hugo Herbelin
2016-01-12Documenting options "Intuition Negation Unfolding", "Intuition Iff Unfolding".Hugo Herbelin
2016-01-12Documenting option 'Set Bracketing Last Introduction Pattern'.Hugo Herbelin
2016-01-12restore documentation of admitEnrico Tassi
2016-01-11Fix bug #3338 again, no progress is necessary for the success of rewrite_strat.Matthieu Sozeau
2016-01-08Be more verbose about failure to compile libraries to native code.Guillaume Melquiond
2016-01-07Fix a misleading comment for substn_varsMatthieu Sozeau
2016-01-07Fix bug #4480: progress was not checked for setoid_rewrite.Matthieu Sozeau
2016-01-06Fix description of command-line options in the manual.Guillaume Melquiond
2016-01-06Prevent coq_makefile from parsing project files in the reverse order. (Fix bu...Guillaume Melquiond
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-25 08:34:17 +0000