aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-17
|\
* | ALPHA-CONVERSION: in the "Reduction" module: clos_fconv --> clos_gen_convGravatar Matej Kosik2015-12-17
* | ALPHA-CONVERSION: in the "Reduction" module: fconv --> gen_convGravatar Matej Kosik2015-12-17
* | CLEANUP: in the Reduction moduleGravatar Matej Kosik2015-12-17
* | CLEANUP: in the Reductionops moduleGravatar Matej Kosik2015-12-17
* | CLEANUP: in the Reduction moduleGravatar Matej Kosik2015-12-17
* | Getting rid of some hardwired generic arguments.Gravatar Pierre-Marie Pédrot2015-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
* | Fixing e3cefca41b about supposingly simplifying primitive projectionsGravatar Hugo Herbelin2015-12-15
* | Fixing unexpected length of context in a typing function, detected byGravatar Hugo Herbelin2015-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
* | Fixing e7f7fc3e058 (wrong chop on contexts). This fixes test-suite.Gravatar Hugo Herbelin2015-12-15
* | API: documenting context_chop and removing a duplicate.Gravatar Hugo Herbelin2015-12-15
| * Changing the order of the goals generated by unshelve.Gravatar Pierre-Marie Pédrot2015-12-15
* | Adding a token "index" representing positions (1st, 2nd, etc.).Gravatar Hugo Herbelin2015-12-15
* | Simplifying documentation of "assert form as pat".Gravatar Hugo Herbelin2015-12-15
* | Granting clear_flag in injection, even legacy mode. This is possibleGravatar Hugo Herbelin2015-12-15
* | Tactics: Generalizing the use of the experimental clearing modifier toGravatar Hugo Herbelin2015-12-15
| * Extraction: replace unused variable names by _ in funs and matchs (fix #2842)Gravatar Pierre Letouzey2015-12-15
* | Revert "Revert PMP's fix of #2498, which introduces an incompatibility with l...Gravatar Pierre-Marie Pédrot2015-12-15
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-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
| * extraction_impl.v: fix a typoGravatar Pierre Letouzey2015-12-14
| * A test file for Extraction Implicit (including bugs #4243 and #4228)Gravatar Pierre Letouzey2015-12-14
| * Extraction: propagate implicit args in inner fixpoint (bug #4243 part 2)Gravatar Pierre Letouzey2015-12-14
* | Adding compatibility flag for 8.5.Gravatar Hugo Herbelin2015-12-14
| * Fix \label which was meants to be \ref in doc of CIC terms.Gravatar Maxime Dénès2015-12-14
| * Remove a mention of Set Virtual Machine in doc.Gravatar Maxime Dénès2015-12-14
| * CoqIDE: add 'you need to restart CoqIDE after changing shortcuts' messageGravatar Enrico Tassi2015-12-14
| * Updating CHANGES with an incompatibility.Gravatar Hugo Herbelin2015-12-14
| * Revert PMP's fix of #2498, which introduces an incompatibility with lablgtkGravatar Maxime Dénès2015-12-14
| * Flag -compat 8.4 now loads Coq.Compat.Coq84.Gravatar Maxime Dénès2015-12-14
| * Moved proof_admitted to its own file, named "AdmitAxiom.v".Gravatar Maxime Dénès2015-12-14
| * Test file for #4363 was not complete.Gravatar Maxime Dénès2015-12-14
| * Extraction: cosmetically avoid generating spaces on empty linesGravatar Pierre Letouzey2015-12-14
* | Remove some occurrences of Unix.opendir.Gravatar Guillaume Melquiond2015-12-14
| * Extraction: also get rid of explicit '\n' for haskellGravatar Pierre Letouzey2015-12-14
| * Extraction: fix a pretty-print issueGravatar Pierre Letouzey2015-12-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-14 20:09:51 +0000