aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
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
2015-01-08Fixing compilation of penultimate commit d08532d.Hugo Herbelin
2015-01-08Avoiding introducing yet another convention in naming files.Hugo Herbelin
2015-01-06Fix setoid rewrite.Arnaud Spiwack
2015-01-03Fixing #3896 (incorrect sigma given to printer).Hugo Herbelin
2014-12-23A global [gfail] tactic which works like [fail] except that it fails even if ...Arnaud Spiwack
2014-12-23Remove compatibility layer from Ltac's [fail].Arnaud Spiwack
2014-12-23Fix compilation error in some configurations.Arnaud Spiwack
2014-12-19Add a backtracking version of Ltac's [match].Arnaud Spiwack
2014-12-18Fixed bad newlines in output for std output and emacs.Pierre Courtieu
2014-12-17Fixing bug #3796.Pierre-Marie Pédrot
2014-12-16Fixing CAMLP4 compilation.Pierre-Marie Pédrot
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
2014-12-12Add Ltac syntax for the [tclIFCATCH] primitive.Arnaud Spiwack
2014-12-12Extend the syntax of simpl with a delta flag.Arnaud Spiwack
2014-12-12In discrimination nets, do not index lambdas if they're part of a betaMatthieu Sozeau
2014-12-11Tentatively more informative report of failure when inferringHugo Herbelin
2014-12-10Fix dummy argument use in guess_elim: there are some cases where X_indMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-12 13:42:27 +0000