aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2015-05-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-05-04Code simplification in Tactics.Pierre-Marie Pédrot
2015-05-01Giving to "subst" a more natural semantic (fixing #4214) by using allHugo Herbelin
2015-04-25Cleaning some uses of exceptions in tactics.Pierre-Marie Pédrot
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
2015-04-23Using tclZEROMSG instead of tclZERO in several places.Pierre-Marie Pédrot
2015-04-22Tactical `progress` compares term up to potentially equalisable universes.Arnaud Spiwack
2015-04-16Ensuring purity of datastructures in the API.Pierre-Marie Pédrot
2015-04-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-04-14Cleaning up the implementation of search entries in Hints.Pierre-Marie Pédrot
2015-04-14Opaque implementation of auto tactics.Pierre-Marie Pédrot
2015-04-13Remove declarations of matched variables in change as an extension ofMatthieu Sozeau
2015-04-13More documented representation of hint objects.Pierre-Marie Pédrot
2015-04-12Making the hint entry type opaque.Pierre-Marie Pédrot
2015-04-10Fix compilation broken by Matthieu's last commit.Pierre Letouzey
2015-04-10Fix #3590 for good this time, by changing the API, change's argument nowMatthieu Sozeau
2015-04-10Eauto hints respect their priority. Fixes bug #3199.Pierre-Marie Pédrot
2015-04-10Making the hints for the auto tactics private.Pierre-Marie Pédrot
2015-04-09Merge branch 'v8.5' into trunkPierre Letouzey
2015-04-09Fix caching of local hintdb in typeclasses eauto.Matthieu Sozeau
2015-04-06refresh metas in rewrite hints loaded from .vo files (fix bug #3815)Nickolai Zeldovich
2015-04-01Removing a probably incorrect on-the-fly require in a tactic.Pierre-Marie Pédrot
2015-03-23Merge branch 'v8.5'Pierre-Marie Pédrot
2015-03-22Aliasing give_up with admitEnrico Tassi
2015-03-11Merge branch 'v8.5'Pierre-Marie Pédrot
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-04Merge branch 'v8.5'Pierre-Marie Pédrot
2015-03-03Fix bug #3590, keeping evars that are not turned into named metas byMatthieu Sozeau
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-20 05:13:16 +0000