aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
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-15Changing the order of the goals generated by unshelve.Pierre-Marie Pédrot
2015-12-15Extraction: replace unused variable names by _ in funs and matchs (fix #2842)Pierre Letouzey
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-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-14Extraction: also get rid of explicit '\n' for haskellPierre Letouzey
2015-12-14Extraction: fix a pretty-print issuePierre Letouzey
2015-12-14Extraction: cleanup a hack (Pp.is_empty instead of Failure "empty phrase")Pierre Letouzey
2015-12-12Extraction: documentation of the new option Unset Extraction SafeImplicitsPierre Letouzey
2015-12-12Extraction: nicer implementation of ImplicitsPierre Letouzey
2015-12-12Extraction: check for remaining implicits after dead code removal (fix #4243)Pierre Letouzey
2015-12-12Extraction: fix for bug #4334 (use of delta_resolver in Extract_env)Pierre Letouzey
2015-12-12Extraction: avoid generating some blanks at end-of-linePierre Letouzey
2015-12-12Indexing and documenting some options.Pierre-Marie Pédrot
2015-12-11Optimize occur_evar_upto_types, avoiding repeateadly looking into theMatthieu Sozeau
2015-12-11Univs: Fix bug #4363, nested abstract.Matthieu Sozeau
2015-12-11Document removal of Set Virtual Machine and -vm in CHANGES.Maxime Dénès
2015-12-11Remove Set Virtual Machine from doc, since the command itself has been removed.Maxime Dénès
2015-12-11Add tactic native_cast_no_check, analog to vm_cast_no_check.Maxime Dénès
2015-12-10Fixing a pat%constr bug. Thanks to Enrico for reporting.Hugo Herbelin
2015-12-10Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.Hugo Herbelin
2015-12-10Fixing compilation with OCaml 3.12 after commit 9d45d45f3a87 on removingHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 10:47:17 +0000