aboutsummaryrefslogtreecommitdiff
path: root/tactics/tactics.ml
AgeCommit message (Expand)Author
2008-06-21- Implantation de la suggestion 1873 sur discriminate. Au final,herbelin
2008-06-18Propagation des révisions 11144 et 11136 de la 8.2 vers le trunkherbelin
2008-06-10- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)herbelin
2008-06-10Backtrack sur l'"optimisation" de admit (révision 11084). Comme leherbelin
2008-06-10- Correction bug 1841 (identificateurs incorrects avec Subclass)herbelin
2008-06-08- Patch sur "intros until 0"herbelin
2008-06-08- Extension de "generalize" en "generalize c as id at occs".herbelin
2008-05-30Improve the dependent induction tactic to automatically find themsozeau
2008-05-07Mises à jour test-suite + amélioration message d'erreur pour non-bug #1757herbelin
2008-04-27- Backtrack sur option with_types suite à confusion sur l'utilisationherbelin
2008-04-26- Backtrack sur extension de syntaxe pour pose qui rentre en conflit avecherbelin
2008-04-23Prise en compte des coercions dans les clauses "with" même si le typeherbelin
2008-04-23Backtrack on change of flags for elim, otherwise rewrite goes undermsozeau
2008-04-23Change default eauto depth to 100 in setoid_rewrite, bump necessarymsozeau
2008-04-21- Parameterize unification by two sets of transparent_state, one for openmsozeau
2008-04-17Bug squashing day !msozeau
2008-04-17Little fixes in setoid_rewrite.msozeau
2008-04-13Bugs, nettoyage, et améliorations diversesherbelin
2008-04-05- Retour en arrière sur la capacité du nouvel apply à utiliser lesherbelin
2008-04-04Mise en place d'une extension de apply pour que celui-ci sacheherbelin
2008-04-04- Relâchement de la contrainte de bonne longueur des intropatternsherbelin
2008-04-04Quelques améliorations des intro patterns:herbelin
2008-04-04Protection de rewrite in contre le dépliage des constantes dans w_unify, ce quiherbelin
2008-04-01Ajout "simple apply" et "simple eapply" pour apply sans unfoldherbelin
2008-03-18Added a function to rebuild an elim scheme from elim_scheme_info. Willcourtieu
2008-03-16Using the "relation" constant made some unifications fail in the newmsozeau
2008-03-15Application de refresh_universes dans typing.ml et retyping.ml : lesherbelin
2008-03-10Pas très propre de reposer sur la capture des anomalies (et celaherbelin
2008-03-07f_equal, revert, specialize in ML, contradict in better Ltac (+doc)letouzey
2008-02-22Merge with lmamane's private branch:lmamane
2008-02-13Essai de prise en compte de delta dans unify_0 (même sur termes non clos). herbelin
2008-02-01Unification de TacLetRecIn et TacLetIn. En particulier, on peutherbelin
2008-01-31Debug implementation of dependent induction/dependent destruction and documen...msozeau
2007-12-31Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...msozeau
2007-12-06Plus de combinateurs sont passés de Util à Option. Le module Options aspiwack
2007-12-05Factorisation des opérations sur le type option de Util dans un module aspiwack
2007-10-24Bugfix in abstract_generalizemsozeau
2007-10-12Uniformisation du comportement de rewrite et rewrite in : quand leherbelin
2007-10-03Ajout de eelim, ecase, edestruct et einduction (expérimental).herbelin
2007-08-07Add a new tactic to generalize an instantiated inductive predicate adding equ...msozeau
2007-07-06New intro pattern "@A", which generates a fresh name based on A.glondu
2007-05-28Retour à un message d'erreur d'apply qui montre un échec sans sans réduction herbelin
2007-05-23A fix for bug #1397: letouzey
2007-05-22Nouvelle stratégie d'unification des types des with-bindings dansherbelin
2007-05-20- Propagation des evars non résolues vers les with_bindings; permet par exempleherbelin
2007-04-28Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.herbelin
2007-04-25New keyword "Inline" for Parameters and Axioms for automatic soubiran
2007-04-16Suite unification apply et eapply (l'un et l'autre profite maintenantherbelin
2007-04-15Essai de partage de code entre apply et eapplyherbelin
2007-04-13Nettoyage des tactiques basées sur "simpl" (delta-réduction cachantherbelin