aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2015-12-17Merge branch 'v8.5'Pierre-Marie Pédrot
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-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-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-08Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-07Fix some typos.Guillaume Melquiond
2015-12-05Removing redundant versions of generalize.Hugo Herbelin
2015-12-05Moving three related small half-general half-ad-hoc utility functionsHugo Herbelin
2015-12-04Getting rid of dynamic hacks in Setoid_newring.Pierre-Marie Pédrot
2015-12-03Removing the last use of tacticIn in setoid_ring.Pierre-Marie Pédrot
2015-11-20Merge branch 'v8.5'Pierre-Marie Pédrot
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-07Preventing an unwanted warning 5 "this function application is partial"Hugo Herbelin
2015-11-07Merge remote-tracking branch 'origin/v8.5' into upstream-trunkHugo Herbelin
2015-11-06Fixing complexity issue with f_equal. Thanks to J.-H. JourdanHugo Herbelin
2015-10-29Monotonizing Tactics.change_arg.Pierre-Marie Pédrot
2015-10-29Removing some goal unsafeness in inductive schemes.Pierre-Marie Pédrot
2015-10-29Merge branch 'v8.5'Pierre-Marie Pédrot
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-20Proofview.Goal.sigma returns an indexed evarmap.Pierre-Marie Pédrot
2015-10-20Indexing Proofview.goals with a stage.Pierre-Marie Pédrot
2015-10-20Boxing the Goal.enter primitive into a record type.Pierre-Marie Pédrot
2015-10-19Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-19Type delayed_open_constr is now monotonic.Pierre-Marie Pédrot
2015-10-19Function debug mode more formatted.Pierre Courtieu
2015-10-19Partly fixes #3225. Removed some old experimental stuff in funind.Pierre Courtieu
2015-10-18Constraining refine to monotonic functions.Pierre-Marie Pédrot
2015-10-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-14Exporting the original unprocessed hint in the hint running function.Pierre-Marie Pédrot
2015-10-13Fix some typos.Guillaume Melquiond
2015-10-09Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-08f_equal fix continued: do a refresh_universes as before.Matthieu Sozeau
2015-10-07Fix bug #4069: f_equal regression.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:34:56 +0000