aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Fixing the Proofview.Goal.goal function.Gravatar Pierre-Marie Pédrot2016-02-17
* Fix bug #4574: Anomaly: Uncaught exception Invalid_argument("splay_arity").Gravatar Pierre-Marie Pédrot2016-02-17
* Do not give a name to anonymous evars anymore. See bug #4547.Gravatar Pierre-Marie Pédrot2016-02-13
* STM: always stock in vio files the first node (state) of a proofGravatar Enrico Tassi2016-02-10
* STM: not delegate proofs that contain Vernac(Module|Require|Import), #4530Gravatar Enrico Tassi2016-02-10
* Don't fail fatally if PATH is not set.Gravatar Emilio Jesus Gallego Arias2016-02-10
* Improving error message with missing patterns in the presence ofGravatar Hugo Herbelin2016-02-08
* Optimizing the universes_of_constr_function.Gravatar Pierre-Marie Pédrot2016-02-03
* Optimizing the computation of frozen evars.Gravatar Pierre-Marie Pédrot2016-02-03
* Opacifying the type of evar naming structure in Evd.Gravatar Pierre-Marie Pédrot2016-02-03
* More compact representation for evar resolvability flag.Gravatar Pierre-Marie Pédrot2016-02-03
* Fix bug #4537: Coq 8.5 is slower in typeclass resolution.Gravatar Pierre-Marie Pédrot2016-01-27
* Fixing bde12b70 about reporting ill-formed constructor.Gravatar Hugo Herbelin2016-01-26
* Tentative fix for bug #4522: Incorrect "Warning..." on windows.Gravatar Pierre-Marie Pédrot2016-01-24
* Fixing bug #4373: coqdep does not know about .vio files.Gravatar Pierre-Marie Pédrot2016-01-24
* Fixing bug #3826: "Incompatible module types" is uninformative.Gravatar Pierre-Marie Pédrot2016-01-24
* Adding a test for bug #4378.Gravatar Pierre-Marie Pédrot2016-01-24
* Fixing bug #4495: Failed assertion in metasyntax.ml.Gravatar Pierre-Marie Pédrot2016-01-24
* Fixing bug #4511: evar tactic can create non-typed evars.Gravatar Pierre-Marie Pédrot2016-01-24
* Fix bug #4503: mixing universe polymorphic and monomorphicGravatar Matthieu Sozeau2016-01-23
* Fix bug #4519: oops, global shadowed local universe level bindings.Gravatar Matthieu Sozeau2016-01-23
* Implement support for universe binder lists in Instance and Program Fixpoint/...Gravatar Matthieu Sozeau2016-01-23
* Fix bug #4506. Using betadeltaiota_nolet might produce terms of the formGravatar Matthieu Sozeau2016-01-23
* Restore warnings produced by the interpretation of the command lineGravatar Hugo Herbelin2016-01-22
* Compile OS X binaries without native_compute support.Gravatar Maxime Dénès2016-01-21
* Update cic.mli MD5 after header update.Gravatar Maxime Dénès2016-01-20
* Update version number in configure.Gravatar Maxime Dénès2016-01-20
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Change $(...)$ to ltac:(...) in section 2.11. Fixes #4500.Gravatar Maxime Dénès2016-01-20
* Documenting Set Bullet Behavior.Gravatar Hugo Herbelin2016-01-20
* Clarifying the documentation of tactics "cbv" and "lazy".Gravatar Hugo Herbelin2016-01-20
* Fixing Not_found on unknown bullet behavior.Gravatar Hugo Herbelin2016-01-20
* Fix bug #4420: check_types was losing universe constraints.Gravatar Matthieu Sozeau2016-01-19
* Thanks Hugo, but let's remain factual.Gravatar Maxime Dénès2016-01-15
* Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Gravatar Maxime Dénès2016-01-15
* Minor edits in output of coqdep --help.Gravatar Maxime Dénès2016-01-15
* Fix #4408.Gravatar Pierre Courtieu2016-01-15
* Partially fixing #4408: coqdep --help is up to date.Gravatar Pierre Courtieu2016-01-15
* MMaps: remove it from final 8.5 release, since this new library isn't mature ...Gravatar Pierre Letouzey2016-01-13
* Fixing success of test for #3848 after move to directory "closed".Gravatar Hugo Herbelin2016-01-13
* Fixing #4467 (continued).Gravatar Hugo Herbelin2016-01-13
* Fixing #4467 (missing shadowing of variables in cases pattern).Gravatar Hugo Herbelin2016-01-12
* Fixing #4256 and #4484 (changes in evar-evar resolution made that newGravatar Hugo Herbelin2016-01-12
* Reporting about the new tactical unshelve.Gravatar Hugo Herbelin2016-01-12
* Extend last commit: keyed unification uses full conversions on the applied co...Gravatar Matthieu Sozeau2016-01-12
* Extend Keyed Unification tests with the one from R. Krebbers.Gravatar Matthieu Sozeau2016-01-12
* Fix essential bug in new Keyed Unification mode reported by R. Krebbers.Gravatar Matthieu Sozeau2016-01-12
* Referring to coq.inria.fr/stdlib for more on libraries and ltac-level tactics.Gravatar Hugo Herbelin2016-01-12
* Documenting dtauto and dintuition.Gravatar Hugo Herbelin2016-01-12
* Documenting options "Intuition Negation Unfolding", "Intuition Iff Unfolding".Gravatar Hugo Herbelin2016-01-12
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 20:11:15 +0000