aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* Adding a test to check whether two tactic notations conflict.Gravatar Pierre-Marie Pédrot2015-05-11
* Fixing bug #4232.Gravatar Pierre-Marie Pédrot2015-05-11
* Rationalizing a bit the interface of Hints.Gravatar Pierre-Marie Pédrot2015-05-11
* Adding a flag "Set Regular Subst Tactic" off by default in v8.5 forGravatar Hugo Herbelin2015-05-09
* Fixing treatment of recursive equations damaged by 857e82b2ca0d1.Gravatar Hugo Herbelin2015-05-06
* Fixing "subst" to respect v8.4 most-ancient to most-recent hyps orderGravatar Hugo Herbelin2015-05-06
* Removing dead code in Rewrite.Gravatar Pierre-Marie Pédrot2015-05-05
* Making the strategy type in Rewrite opaque.Gravatar Pierre-Marie Pédrot2015-05-05
* Code simplification in Tactics.Gravatar Pierre-Marie Pédrot2015-05-04
* Giving to "subst" a more natural semantic (fixing #4214) by using allGravatar Hugo Herbelin2015-05-01
* Cleaning some uses of exceptions in tactics.Gravatar Pierre-Marie Pédrot2015-04-25
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
* Using tclZEROMSG instead of tclZERO in several places.Gravatar Pierre-Marie Pédrot2015-04-23
* Tactical `progress` compares term up to potentially equalisable universes.Gravatar Arnaud Spiwack2015-04-22
* Ensuring purity of datastructures in the API.Gravatar Pierre-Marie Pédrot2015-04-16
* Cleaning up the implementation of search entries in Hints.Gravatar Pierre-Marie Pédrot2015-04-14
* Opaque implementation of auto tactics.Gravatar Pierre-Marie Pédrot2015-04-14
* Remove declarations of matched variables in change as an extension ofGravatar Matthieu Sozeau2015-04-13
* More documented representation of hint objects.Gravatar Pierre-Marie Pédrot2015-04-13
* Making the hint entry type opaque.Gravatar Pierre-Marie Pédrot2015-04-12
* Fix compilation broken by Matthieu's last commit.Gravatar Pierre Letouzey2015-04-10
* Fix #3590 for good this time, by changing the API, change's argument nowGravatar Matthieu Sozeau2015-04-10
* Eauto hints respect their priority. Fixes bug #3199.Gravatar Pierre-Marie Pédrot2015-04-10
* Making the hints for the auto tactics private.Gravatar Pierre-Marie Pédrot2015-04-10
* Fix caching of local hintdb in typeclasses eauto.Gravatar Matthieu Sozeau2015-04-09
* refresh metas in rewrite hints loaded from .vo files (fix bug #3815)Gravatar Nickolai Zeldovich2015-04-06
* Removing a probably incorrect on-the-fly require in a tactic.Gravatar Pierre-Marie Pédrot2015-04-01
* Aliasing give_up with admitGravatar Enrico Tassi2015-03-22
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
* Reverting r10021 which enforces early assumptions on freshness whichGravatar Hugo Herbelin2015-03-07
* Continuing a8ad3abc15a2 and 60810aaec on freshness of name in tactic "evar".Gravatar Hugo Herbelin2015-03-07
* Fix bug #3590, keeping evars that are not turned into named metas byGravatar Matthieu Sozeau2015-03-03
* Removing the unused field ltacrecvars of tactic internalization.Gravatar Pierre-Marie Pédrot2015-02-27
* Hack so that refine_no_check accepts an argument which is a match on anGravatar Hugo Herbelin2015-02-27
* Somehow fixing bug #3467.Gravatar Pierre-Marie Pédrot2015-02-27
* Fixing bug #3298.Gravatar Pierre-Marie Pédrot2015-02-26
* Fixing printing of ordinals.Gravatar Pierre-Marie Pédrot2015-02-26
* [info_auto] & [info_trivial]: warning message to help users find [Info].Gravatar Arnaud Spiwack2015-02-24
* [info] tactical warning: do not suggest [info_auto] and [info_trivial].Gravatar Arnaud Spiwack2015-02-24
* Fix some typos in comments.Gravatar Guillaume Melquiond2015-02-23
* Fixing error message when H already exists in tactic subexpression eqn:H.Gravatar Hugo Herbelin2015-02-20
* A fix for #3993 (not fully applied term to destruct when eqn is given).Gravatar Hugo Herbelin2015-02-20
* Fix bug #3938Gravatar Matthieu Sozeau2015-02-18
* Fixing bug #3944.Gravatar Pierre-Marie Pédrot2015-02-16
* Fixing bug #4016.Gravatar Pierre-Marie Pédrot2015-02-14
* Univs: fix bug #4031: wrong folding of sigma in change.Gravatar Matthieu Sozeau2015-02-12
* Fix bug #2775: Correct handling of universes in leminv.Gravatar Matthieu Sozeau2015-02-12
* Fixing compilation for 3.12.Gravatar Pierre-Marie Pédrot2015-02-12
* Tentative fix for bug #4027.Gravatar Pierre-Marie Pédrot2015-02-12
* Missing space in error messageGravatar Matěj Grabovský2015-02-11
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-27 00:46:17 +0000