aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2016-09-03Fixing what is probably a typo in Strict Proofs mode (#5062).Hugo Herbelin
2016-08-30micromega cache files are now hidden files (cf #4156)Frédéric Besson
2016-07-06improved complexity in nsatzthery
2016-07-06Bug Fixes : 4851 4858 4880 for nsatzthery
2016-07-05Bug fix : variable capture in ltac code of Nsatzthery
2016-07-04congruence: Restrict refreshing to SetMatthieu Sozeau
2016-07-04congruence: remove casts of indexed termsMatthieu Sozeau
2016-07-04congruence/univs: properly refresh (fix #4609)Matthieu Sozeau
2016-06-23Fix typo.Guillaume Melquiond
2016-06-14Merge branch 'bug4725' into v8.5Matthieu Sozeau
2016-05-30Extraction : add a location in the error message about polypropPierre Letouzey
2016-05-26Univs/Program/Function: Fix bug #4725Matthieu Sozeau
2016-05-23Extraction/Projections: Fix bug #4710Matthieu Sozeau
2016-05-20Disable memoization rather than failing when files cannot be opened.Guillaume Melquiond
2016-05-19Extraction: don't call Unicode.ascii_of_ident twice (not idempotent anymore)Pierre Letouzey
2016-05-04Fix Haskell extraction for terms over 45 characters longNickolai Zeldovich
2016-05-04Handle primitive projections inside types when extracting (bug #4616).Guillaume Melquiond
2016-05-03Remove extraneous space in coqtop/pg output (bug #4675).Guillaume Melquiond
2016-04-09Fix order of arguments to Big.compare_case in ExtrOcamlZBigInt.vNickolai Zeldovich
2016-04-08Fixing a source of inefficiency and an artificial dependency in theDaniel de Rauglaudre
2016-03-04Rename Ephemeron -> CEphemeron.Maxime Dénès
2016-01-20Update copyright headers.Maxime Dénès
2016-01-15Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Maxime Dénès
2016-01-06Protect code against changes in Map interface.Maxime Dénès
2016-01-04Extraction: msg_notice instead of msg_info.Pierre Courtieu
2015-12-22Inclusion of functors with restricted signature is now forbidden (fix #3746)Pierre Letouzey
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-15Extraction: more cautious use of intermediate result caching (fix #3923)Pierre Letouzey
2015-12-15Extraction: fix a few little glitches with my last commit (replacing unused v...Pierre Letouzey
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-14Extraction: propagate implicit args in inner fixpoint (bug #4243 part 2)Pierre Letouzey
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: 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-07Fix some typos.Guillaume Melquiond
2015-11-19Fix bug #4433, removing hack on evars appearing in a pattern from aMatthieu Sozeau
2015-11-18Fix a bug preventing the generation of graphs when doing multipleMatthieu Sozeau
2015-11-06Fixing complexity issue with f_equal. Thanks to J.-H. JourdanHugo Herbelin
2015-10-28Univs: local names handling.Matthieu Sozeau
2015-10-28Avoid type checking private_constants (side_eff) again during Qed (#4357).Enrico Tassi
2015-10-28Univs: fix bug #4375, accept universe binders on (co)-fixpointsMatthieu Sozeau
2015-10-28Do not pause globing in funind. (Fix bug #4382)Guillaume Melquiond
2015-10-19Partly fixes #3225. Removed some old experimental stuff in funind.Pierre Courtieu
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-04 05:19:40 +0000