aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tactics.ml
Commit message (Expand)AuthorAge
...
* Modification rapide du message d'erreur lorsqu'un _ ne peut êtreGravatar herbelin2008-07-18
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* - Implantation de la suggestion 1873 sur discriminate. Au final,Gravatar herbelin2008-06-21
* Propagation des révisions 11144 et 11136 de la 8.2 vers le trunkGravatar herbelin2008-06-18
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
* Backtrack sur l'"optimisation" de admit (révision 11084). Comme leGravatar herbelin2008-06-10
* - Correction bug 1841 (identificateurs incorrects avec Subclass)Gravatar herbelin2008-06-10
* - Patch sur "intros until 0"Gravatar herbelin2008-06-08
* - Extension de "generalize" en "generalize c as id at occs".Gravatar herbelin2008-06-08
* Improve the dependent induction tactic to automatically find theGravatar msozeau2008-05-30
* Mises à jour test-suite + amélioration message d'erreur pour non-bug #1757Gravatar herbelin2008-05-07
* - Backtrack sur option with_types suite à confusion sur l'utilisationGravatar herbelin2008-04-27
* - Backtrack sur extension de syntaxe pour pose qui rentre en conflit avecGravatar herbelin2008-04-26
* Prise en compte des coercions dans les clauses "with" même si le typeGravatar herbelin2008-04-23
* Backtrack on change of flags for elim, otherwise rewrite goes underGravatar msozeau2008-04-23
* Change default eauto depth to 100 in setoid_rewrite, bump necessaryGravatar msozeau2008-04-23
* - Parameterize unification by two sets of transparent_state, one for openGravatar msozeau2008-04-21
* Bug squashing day !Gravatar msozeau2008-04-17
* Little fixes in setoid_rewrite.Gravatar msozeau2008-04-17
* Bugs, nettoyage, et améliorations diversesGravatar herbelin2008-04-13
* - Retour en arrière sur la capacité du nouvel apply à utiliser lesGravatar herbelin2008-04-05
* Mise en place d'une extension de apply pour que celui-ci sacheGravatar herbelin2008-04-04
* - Relâchement de la contrainte de bonne longueur des intropatternsGravatar herbelin2008-04-04
* Quelques améliorations des intro patterns:Gravatar herbelin2008-04-04
* Protection de rewrite in contre le dépliage des constantes dans w_unify, ce quiGravatar herbelin2008-04-04
* Ajout "simple apply" et "simple eapply" pour apply sans unfoldGravatar herbelin2008-04-01
* Added a function to rebuild an elim scheme from elim_scheme_info. WillGravatar courtieu2008-03-18
* Using the "relation" constant made some unifications fail in the newGravatar msozeau2008-03-16
* Application de refresh_universes dans typing.ml et retyping.ml : lesGravatar herbelin2008-03-15
* Pas très propre de reposer sur la capture des anomalies (et celaGravatar herbelin2008-03-10
* f_equal, revert, specialize in ML, contradict in better Ltac (+doc)Gravatar letouzey2008-03-07
* Merge with lmamane's private branch:Gravatar lmamane2008-02-22
* Essai de prise en compte de delta dans unify_0 (même sur termes non clos). Gravatar herbelin2008-02-13
* Unification de TacLetRecIn et TacLetIn. En particulier, on peutGravatar herbelin2008-02-01
* Debug implementation of dependent induction/dependent destruction and documen...Gravatar msozeau2008-01-31
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
* Bugfix in abstract_generalizeGravatar msozeau2007-10-24
* Uniformisation du comportement de rewrite et rewrite in : quand leGravatar herbelin2007-10-12
* Ajout de eelim, ecase, edestruct et einduction (expérimental).Gravatar herbelin2007-10-03
* Add a new tactic to generalize an instantiated inductive predicate adding equ...Gravatar msozeau2007-08-07
* New intro pattern "@A", which generates a fresh name based on A.Gravatar glondu2007-07-06
* Retour à un message d'erreur d'apply qui montre un échec sans sans réduction Gravatar herbelin2007-05-28
* A fix for bug #1397: Gravatar letouzey2007-05-23
* Nouvelle stratégie d'unification des types des with-bindings dansGravatar herbelin2007-05-22
* - Propagation des evars non résolues vers les with_bindings; permet par exempleGravatar herbelin2007-05-20
* Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.Gravatar herbelin2007-04-28
* New keyword "Inline" for Parameters and Axioms for automatic Gravatar soubiran2007-04-25
* Suite unification apply et eapply (l'un et l'autre profite maintenantGravatar herbelin2007-04-16