aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* 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
* Documenting option 'Set Bracketing Last Introduction Pattern'.Gravatar Hugo Herbelin2016-01-12
* restore documentation of admitGravatar Enrico Tassi2016-01-12
* Fix bug #3338 again, no progress is necessary for the success of rewrite_strat.Gravatar Matthieu Sozeau2016-01-11
* Be more verbose about failure to compile libraries to native code.Gravatar Guillaume Melquiond2016-01-08
* Fix a misleading comment for substn_varsGravatar Matthieu Sozeau2016-01-07
* Fix bug #4480: progress was not checked for setoid_rewrite.Gravatar Matthieu Sozeau2016-01-07
* Fix description of command-line options in the manual.Gravatar Guillaume Melquiond2016-01-06
* Prevent coq_makefile from parsing project files in the reverse order. (Fix bu...Gravatar Guillaume Melquiond2016-01-06
* Protect code against changes in Map interface.Gravatar Maxime Dénès2016-01-06
* Disable warning 31 when generating coqtop from coqmktop.Gravatar Maxime Dénès2016-01-05
* Avoid warning 31: test printer was linked twice with Dynlink and Str.Gravatar Maxime Dénès2016-01-05
* Fix order of files in mllib.Gravatar Maxime Dénès2016-01-05
* COMMENTS: PredicateGravatar Matej Kosik2016-01-05
* fixup d2b468a, evar normalization is neededGravatar Enrico Tassi2016-01-04
* Extraction: msg_notice instead of msg_info.Gravatar Pierre Courtieu2016-01-04
* Fix handling of side-effects in case of `Opaque side-effects as well.Gravatar Matthieu Sozeau2016-01-04
* par: check if the goal is not ground and fail (fix #4465)Gravatar Enrico Tassi2016-01-04
* workers: purge short version of -load-vernac too (fix #4458)Gravatar Enrico Tassi2016-01-04
* Put implicits back as in 8.4.Gravatar Matthieu Sozeau2015-12-31
* Fix bug #4456, anomaly in handle-side effectsGravatar Matthieu Sozeau2015-12-31
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 20:37:08 +0000