aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
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
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
2014-12-09Switch the few remaining iso-latin-1 files to utf8Pierre Letouzey
2014-12-08This is for documenting and slightly fixing commits 547e97e, c52aea7, 9a34d3e.Hugo Herbelin
2014-12-08Constructor tactics backtracking is done using [Tacticals.New] rather than [P...Arnaud Spiwack
2014-12-07Step 4 : atomize_thenHugo Herbelin
2014-12-07Step 2Hugo Herbelin
2014-12-07Step 1Hugo Herbelin
2014-12-07Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic.Hugo Herbelin
2014-12-07Exporting store of goals so that new_evar in convert, intro, etc. canHugo Herbelin
2014-12-02For compatibility purpose, when setoid_rewriting a hypothesis, beta-iotaPierre-Marie Pédrot
2014-12-01More invariants in the code of Rewrite.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 10:55:18 +0000