aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* Fixing incompatibility introduced with simpl in commit 364decf59c1 (orGravatar Hugo Herbelin2015-06-23
* With the field record punning syntax.Gravatar Theo Zimmermann2015-06-23
* Put all arguments of strategy in record.Gravatar Theo Zimmermann2015-06-23
* Strategy is now a record type with a function field.Gravatar Theo Zimmermann2015-06-23
* Add comments.Gravatar Theo Zimmermann2015-06-23
* Fix bug #4159Gravatar Matthieu Sozeau2015-05-27
* Fixing bug #2814: "Anomaly: Uncaught exception Option.IsNone".Gravatar Pierre-Marie Pédrot2015-05-16
* Granting wish #4048: Locate Ltac prints the source of redefined Ltac.Gravatar Pierre-Marie Pédrot2015-05-15
* Fixing bug #4216:Gravatar Pierre-Marie Pédrot2015-05-13
* Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
* Adding an option Loose Hint Behavior to handle hints loaded but not imported.Gravatar Pierre-Marie Pédrot2015-05-12
* Adding unique identifiers to hints.Gravatar Pierre-Marie Pédrot2015-05-12
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 18:10:51 +0000