aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacticals.ml
Commit message (Expand)AuthorAge
* Use a lazy value for the message in FailError, so that it won't beGravatar msozeau2009-06-11
* Fixing bug #2308 ("instantiate" tactic did not comply withGravatar herbelin2009-04-24
* Uniformizing Tacticals, continued (allClauses -> allHypsAndConcl)Gravatar herbelin2009-03-17
* Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"Gravatar herbelin2009-03-16
* Cleaning/uniformizing the interface of tacticals.mliGravatar herbelin2009-03-14
* Petit nettoyage faisant suite au commit #11847 .Gravatar aspiwack2009-01-23
* - Temptative change to notations like "as [|n H]_eqn" or "as [|n H]_eqn:H",Gravatar herbelin2009-01-02
* - Extracted from the tactic "now" an experimental tactic "easy" for smallGravatar herbelin2008-12-26
* - Optimized "auto decomp" which had a (presumably) exponential inGravatar herbelin2008-12-26
* Affichage des notations récursives:Gravatar herbelin2008-10-22
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* 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
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
* - 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
* Bugs, nettoyage, et améliorations diversesGravatar herbelin2008-04-13
* Mise en place d'une extension de apply pour que celui-ci sacheGravatar herbelin2008-04-04
* Adding the tactic "instantiate" (without argument), to force theGravatar glondu2007-12-07
* Nouvelle stratégie d'unification des types des with-bindings dansGravatar herbelin2007-05-22
* revision de la semantique de rewrite ... in <clause>. details dans la docGravatar letouzey2006-10-05
* Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...Gravatar herbelin2006-05-30
* Messages de idtac et fail peuvent maintenant être des listes de string, int ...Gravatar herbelin2006-01-21
* Ajout motif d'introduction "?" (IntroAnonymous) pour laisser CoqGravatar herbelin2006-01-16
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Types inductifs parametriquesGravatar mohring2005-11-02
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* hiding the meta_map in evar_defsGravatar barras2004-09-15
* simplification de clenvGravatar barras2004-09-10
* unification encore...Gravatar barras2004-09-08
* deuxieme vague de modifs: evar_defs fonctionnelGravatar barras2004-09-07
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
* Nouvelle en-têteGravatar herbelin2004-07-16
* Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id va...Gravatar herbelin2004-03-02
* Déplacement définition intro_pattern_expr dans GenargGravatar herbelin2004-03-01
* factorisation et generalisation des clausesGravatar barras2003-11-13
* Idtac peut prendre un argument à afficherGravatar narboux2003-11-12
* Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'Gravatar herbelin2003-10-10
* Indépendance vis à vis de DeclareGravatar herbelin2003-09-12
* Ground Update.Gravatar corbinea2003-06-20
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* Ajout d'un message à FailTacGravatar herbelin2003-03-31
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Réorganisation des tclTHEN (cf dev/changements.txt)Gravatar herbelin2002-05-29
* Nouveau Rewrite-in plus economiqueGravatar barras2002-03-04
* Elim dependente n'appelait pas la bonne fonction pour calculer le predicatGravatar barras2002-02-19
* petits changements cosmetiques sur les tactiquesGravatar barras2002-02-15
* - Reforme de la gestion des args recursifs (via arbres reguliers)Gravatar barras2002-02-14
* Ajout tactiques Rename et Pose; modifications pour InversionGravatar herbelin2002-02-01