aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* Univs: refined handling of assumptionsGravatar Matthieu Sozeau2015-10-02
* Univs: fix evar_map handling in Hint processing.Gravatar Matthieu Sozeau2015-10-02
* discriminate: Do fresh_global in the right env in presence of side-effects.Gravatar Matthieu Sozeau2015-10-02
* Univs: fix many evar_map initializations and leaks.Gravatar Matthieu Sozeau2015-10-02
* Hopefully better names to constructors of internal_flag, as discussedGravatar Hugo Herbelin2015-09-23
* Give a way to control if the decidable-equality schemes are built likeGravatar Hugo Herbelin2015-09-23
* Fixing bug #4207: setoid_rewrite creates self-referring hypotheses.Gravatar Pierre-Marie Pédrot2015-09-22
* In pat/constr introduction patterns, fixing in a better way clearing problemsGravatar Hugo Herbelin2015-09-16
* Continuing investigation on how to preserve the locality of the actionGravatar Hugo Herbelin2015-09-16
* Univs: Add universe binding lists to definitionsGravatar Matthieu Sozeau2015-09-14
* Fixing incomplete bugfix in 76f27140e6e34 (unfortunately 5 commitsGravatar Hugo Herbelin2015-09-08
* Ensuring that patterns of the form pat/constr move the hypotheses replacingGravatar Hugo Herbelin2015-09-08
* Short cosmetic changes in tactics.ml.Gravatar Hugo Herbelin2015-09-08
* A bit of documentation of OCaml code for intro_patterns.Gravatar Hugo Herbelin2015-09-08
* New option "Unset Bracketing Last Introduction Pattern" for preservingGravatar Hugo Herbelin2015-09-08
* Fixing clearing of temporary hypotheses with intro pattern pat/constr.Gravatar Hugo Herbelin2015-09-08
* Fixing "pose proof (H ...) as H" and "assert (H:=H ...) which were supposedGravatar Hugo Herbelin2015-09-08
* 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
* 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
* class_tactics: make interruptibleGravatar Enrico Tassi2015-06-29
* class_tactics: remove catch-all, use Errors.noncriticalGravatar Enrico Tassi2015-06-29
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 03:50:19 +0000