aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* 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
* Do not dump a glob reference when its location is ghost. (Fix bug #4469)Gravatar Guillaume Melquiond2015-12-31
* Fixing bug #4462: unshelve: Anomaly: Uncaught exception Not_found.Gravatar Pierre-Marie Pédrot2015-12-29
* Inclusion of functors with restricted signature is now forbidden (fix #3746)Gravatar Pierre Letouzey2015-12-22
* (Partial) fix for bug #4453: raise an error instead of an anomaly.Gravatar Matthieu Sozeau2015-12-17
* spawn: fix leak of file descriptorsGravatar Enrico Tassi2015-12-17
* Updating credits.Gravatar Hugo Herbelin2015-12-16
* Update version numbers and magic numbers for 8.5rc1 release.Gravatar Maxime Dénès2015-12-16
* FIx parsing of tactic "simple refine".Gravatar Maxime Dénès2015-12-16
* Add a "simple refine" variant of "refine" that does not call "shelve_unifiable".Gravatar Guillaume Melquiond2015-12-16
* Extraction: slightly better heuristic for Obj.magic simplificationsGravatar Pierre Letouzey2015-12-16
* Extraction: fixed beta-red with Obj.magic (#2795 again) + other simplificationsGravatar Pierre Letouzey2015-12-16
* Proof using: do not clear unused section hyps automaticallyGravatar Enrico Tassi2015-12-15
* Fix test suite after change in extraction.Gravatar Maxime Dénès2015-12-15
* Extraction: more cautious use of intermediate result caching (fix #3923)Gravatar Pierre Letouzey2015-12-15
* Fix test-suite files after change in refine tactic.Gravatar Maxime Dénès2015-12-15
* Extraction: fix a few little glitches with my last commit (replacing unused v...Gravatar Pierre Letouzey2015-12-15
* Adding a test for the unshelve tactical.Gravatar Pierre-Marie Pédrot2015-12-15
* Refine tactic now shelves unifiable holes.Gravatar Pierre-Marie Pédrot2015-12-15
* Changing the order of the goals generated by unshelve.Gravatar Pierre-Marie Pédrot2015-12-15
* Extraction: replace unused variable names by _ in funs and matchs (fix #2842)Gravatar Pierre Letouzey2015-12-15
* Extraction: allow basic beta-reduction even through a MLmagic (fix #2795)Gravatar Pierre Letouzey2015-12-14
* Fixing little bug of coq_makefile with unterminated comment.Gravatar Hugo Herbelin2015-12-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 03:19:44 +0000