aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2015-03-22Aliasing give_up with admitEnrico Tassi
2015-03-11admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Enrico Tassi
2015-03-07Reverting r10021 which enforces early assumptions on freshness whichHugo Herbelin
2015-03-07Continuing a8ad3abc15a2 and 60810aaec on freshness of name in tactic "evar".Hugo Herbelin
2015-03-03Fix bug #3590, keeping evars that are not turned into named metas byMatthieu Sozeau
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-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-23Fix some typos in comments.Guillaume Melquiond
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-18Fix bug #3938Matthieu Sozeau
2015-02-16Fixing bug #3944.Pierre-Marie Pédrot
2015-02-14Fixing bug #4016.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-10Fixing #4018 (uncaught exception on non-equality in intros [=]).Hugo Herbelin
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-24Removed obsolete option "Legacy Partially Applied EliminationHugo Herbelin
2015-01-24Tentative workaround for bug #3798.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 11:10:50 +0000