aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2015-02-28Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-27Removing the unused field ltacrecvars of tactic internalization.Pierre-Marie Pédrot
2015-02-27Hack so that refine_no_check accepts an argument which is a match on anHugo Herbelin
2015-02-27Somehow fixing bug #3467.Pierre-Marie Pédrot
2015-02-26Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-26Fixing bug #3298.Pierre-Marie Pédrot
2015-02-26Fixing printing of ordinals.Pierre-Marie Pédrot
2015-02-24[info_auto] & [info_trivial]: warning message to help users find [Info].Arnaud Spiwack
2015-02-24[info] tactical warning: do not suggest [info_auto] and [info_trivial].Arnaud Spiwack
2015-02-23Merge branch 'v8.5' into trunkEnrico Tassi
2015-02-23Fix some typos in comments.Guillaume Melquiond
2015-02-23Less compatibility layer in Eauto.Pierre-Marie Pédrot
2015-02-23Partially porting eauto to the new tactic API.Pierre-Marie Pédrot
2015-02-23Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-20Fixing error message when H already exists in tactic subexpression eqn:H.Hugo Herbelin
2015-02-20A fix for #3993 (not fully applied term to destruct when eqn is given).Hugo Herbelin
2015-02-18Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-18Fix bug #3938Matthieu Sozeau
2015-02-16Fixing bug #3944.Pierre-Marie Pédrot
2015-02-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-14Fixing bug #4016.Pierre-Marie Pédrot
2015-02-13Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-12Univs: fix bug #4031: wrong folding of sigma in change.Matthieu Sozeau
2015-02-12Fix bug #2775: Correct handling of universes in leminv.Matthieu Sozeau
2015-02-12Fixing compilation for 3.12.Pierre-Marie Pédrot
2015-02-12Tentative fix for bug #4027.Pierre-Marie Pédrot
2015-02-11Missing space in error messageMatěj Grabovský
2015-02-11Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-10Fixing #4018 (uncaught exception on non-equality in intros [=]).Hugo Herbelin
2015-02-10Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-10More expressive API for tclWITHHOLES.Pierre-Marie Pédrot
2015-02-10Revert "Removing spurious tclWITHHOLES."Pierre-Marie Pédrot
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-25Merge branch 'v8.5' into trunk.Pierre-Marie Pédrot
2015-01-24Removed obsolete option "Legacy Partially Applied EliminationHugo Herbelin
2015-01-24Tentative workaround for bug #3798.Pierre-Marie Pédrot
2015-01-23Splitting ML tactics in one function per grammar entry.Pierre-Marie Pédrot
2015-01-21Embedding the index of the ML tactic entry in the Tacexpr AST.Pierre-Marie Pédrot
2015-01-18Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
2015-01-18Make native compiler handle universe polymorphic definitions.Maxime Dénès
2015-01-18Revert "TCs: Properly handle Hint Extern with conclusions of the form _ -> _"Matthieu Sozeau
2015-01-18Add a (by default deactivated) option to force typeclass resolution toMatthieu Sozeau
2015-01-18Optionally allow eta-conversion during unification for type classes.Matthieu Sozeau
2015-01-17Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
2015-01-17Make native compiler handle universe polymorphic definitions.Maxime Dénès
2015-01-16Revert "TCs: Properly handle Hint Extern with conclusions of the form _ -> _"Matthieu Sozeau
2015-01-15Add a (by default deactivated) option to force typeclass resolution toMatthieu Sozeau
2015-01-15Optionally allow eta-conversion during unification for type classes.Matthieu Sozeau
2015-01-13TCs: Properly handle Hint Extern with conclusions of the form _ -> _Matthieu Sozeau
2015-01-12Update headers.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 14:05:52 +0000