aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2016-01-06Protect code against changes in Map interface.Maxime Dénès
2016-01-05Disable warning 31 when generating coqtop from coqmktop.Maxime Dénès
2016-01-05Avoid warning 31: test printer was linked twice with Dynlink and Str.Maxime Dénès
2016-01-05Fix order of files in mllib.Maxime Dénès
2016-01-05COMMENTS: PredicateMatej Kosik
2016-01-04fixup d2b468a, evar normalization is neededEnrico Tassi
2016-01-04Extraction: msg_notice instead of msg_info.Pierre Courtieu
2016-01-04Fix handling of side-effects in case of `Opaque side-effects as well.Matthieu Sozeau
2016-01-04par: check if the goal is not ground and fail (fix #4465)Enrico Tassi
2016-01-04workers: purge short version of -load-vernac too (fix #4458)Enrico Tassi
2015-12-31Put implicits back as in 8.4.Matthieu Sozeau
2015-12-31Fix bug #4456, anomaly in handle-side effectsMatthieu Sozeau
2015-12-31Do not dump a glob reference when its location is ghost. (Fix bug #4469)Guillaume Melquiond
2015-12-29Fixing bug #4462: unshelve: Anomaly: Uncaught exception Not_found.Pierre-Marie Pédrot
2015-12-22Inclusion of functors with restricted signature is now forbidden (fix #3746)Pierre Letouzey
2015-12-17(Partial) fix for bug #4453: raise an error instead of an anomaly.Matthieu Sozeau
2015-12-17spawn: fix leak of file descriptorsEnrico Tassi
2015-12-16Updating credits.Hugo Herbelin
2015-12-16Update version numbers and magic numbers for 8.5rc1 release.Maxime Dénès
2015-12-16FIx parsing of tactic "simple refine".Maxime Dénès
2015-12-16Add a "simple refine" variant of "refine" that does not call "shelve_unifiable".Guillaume Melquiond
2015-12-16Extraction: slightly better heuristic for Obj.magic simplificationsPierre Letouzey
2015-12-16Extraction: fixed beta-red with Obj.magic (#2795 again) + other simplificationsPierre Letouzey
2015-12-15Proof using: do not clear unused section hyps automaticallyEnrico Tassi
2015-12-15Fix test suite after change in extraction.Maxime Dénès
2015-12-15Extraction: more cautious use of intermediate result caching (fix #3923)Pierre Letouzey
2015-12-15Fix test-suite files after change in refine tactic.Maxime Dénès
2015-12-15Extraction: fix a few little glitches with my last commit (replacing unused v...Pierre Letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 03:52:58 +0000