aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* Allowing the abstract tactical to clear the environment from unused variables.Gravatar Pierre-Marie Pédrot2015-08-22
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-08-05
|\
| * Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
| * Give a way to control if the decidable-equality schemes are built likeGravatar Hugo Herbelin2015-08-02
| * Granting Jason's request for an ad hoc compatibility option onGravatar Hugo Herbelin2015-08-02
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-07-29
|\|
| * Fix for bug #4280: "decide equality produces terms that don't compute well".Gravatar Pierre-Marie Pédrot2015-07-28
| * Fixing bug #3509 and #3510 (anomalies in "tactics/term_dnet.ml").Gravatar Pierre-Marie Pédrot2015-07-28
* | Add an Iterative Deepening search strategy to typeclass resolution.Gravatar Matthieu Sozeau2015-07-27
* | Merge branch 'v8.5' into trunkGravatar Maxime Dénès2015-07-02
|\|
| * class_tactics: make interruptibleGravatar Enrico Tassi2015-06-29
| * class_tactics: remove catch-all, use Errors.noncriticalGravatar Enrico Tassi2015-06-29
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-06-24
|\|
| * 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
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-06-01
|\|
| * 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
* | Turning "Set Regular Subst Tactic" on by default (for 8.6).Gravatar Hugo Herbelin2015-05-15
* | Merge v8.5 into trunkGravatar Hugo Herbelin2015-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
* | Merge branch 'v8.5'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
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-04-15
|\|
| * 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