aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-12-18COMMENTS: added to the "Names" module.Matej Kosik
2015-12-18Tying the loop in tactic printing API.Pierre-Marie Pédrot
2015-12-17Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-17ALPHA-CONVERSION: in the "Reduction" module: clos_fconv --> clos_gen_convMatej Kosik
2015-12-17ALPHA-CONVERSION: in the "Reduction" module: fconv --> gen_convMatej Kosik
2015-12-17CLEANUP: in the Reduction moduleMatej Kosik
2015-12-17CLEANUP: in the Reductionops moduleMatej Kosik
2015-12-17CLEANUP: in the Reduction moduleMatej Kosik
2015-12-17Getting rid of some hardwired generic arguments.Pierre-Marie Pédrot
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
2015-12-15Fixing e3cefca41b about supposingly simplifying primitive projectionsHugo Herbelin
2015-12-15Fixing unexpected length of context in a typing function, detected byHugo Herbelin
2015-12-15Adding a test for the unshelve tactical.Pierre-Marie Pédrot
2015-12-15Refine tactic now shelves unifiable holes.Pierre-Marie Pédrot
2015-12-15Fixing e7f7fc3e058 (wrong chop on contexts). This fixes test-suite.Hugo Herbelin
2015-12-15API: documenting context_chop and removing a duplicate.Hugo Herbelin
2015-12-15Changing the order of the goals generated by unshelve.Pierre-Marie Pédrot
2015-12-15Adding a token "index" representing positions (1st, 2nd, etc.).Hugo Herbelin
2015-12-15Simplifying documentation of "assert form as pat".Hugo Herbelin
2015-12-15Granting clear_flag in injection, even legacy mode. This is possibleHugo Herbelin
2015-12-15Tactics: Generalizing the use of the experimental clearing modifier toHugo Herbelin
2015-12-15Extraction: replace unused variable names by _ in funs and matchs (fix #2842)Pierre Letouzey
2015-12-15Revert "Revert PMP's fix of #2498, which introduces an incompatibility with l...Pierre-Marie Pédrot
2015-12-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-14Extraction: allow basic beta-reduction even through a MLmagic (fix #2795)Pierre Letouzey
2015-12-14Fixing little bug of coq_makefile with unterminated comment.Hugo Herbelin
2015-12-14extraction_impl.v: fix a typoPierre Letouzey
2015-12-14A test file for Extraction Implicit (including bugs #4243 and #4228)Pierre Letouzey
2015-12-14Extraction: propagate implicit args in inner fixpoint (bug #4243 part 2)Pierre Letouzey
2015-12-14Adding compatibility flag for 8.5.Hugo Herbelin
2015-12-14Fix \label which was meants to be \ref in doc of CIC terms.Maxime Dénès
2015-12-14Remove a mention of Set Virtual Machine in doc.Maxime Dénès
2015-12-14CoqIDE: add 'you need to restart CoqIDE after changing shortcuts' messageEnrico Tassi
2015-12-14Updating CHANGES with an incompatibility.Hugo Herbelin
2015-12-14Revert PMP's fix of #2498, which introduces an incompatibility with lablgtkMaxime Dénès
2015-12-14Flag -compat 8.4 now loads Coq.Compat.Coq84.Maxime Dénès
2015-12-14Moved proof_admitted to its own file, named "AdmitAxiom.v".Maxime Dénès
2015-12-14Test file for #4363 was not complete.Maxime Dénès
2015-12-14Extraction: cosmetically avoid generating spaces on empty linesPierre Letouzey
2015-12-14Remove some occurrences of Unix.opendir.Guillaume Melquiond
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-21 12:41:13 +0000