aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacticals.ml
Commit message (Expand)AuthorAge
* 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
* Bug calcul de la signature incorrecte en présence de letinGravatar herbelin2002-01-24
* Suppression des stamps et donc des *_constraintsGravatar clrenard2001-11-12
* GROS COMMIT:Gravatar barras2001-11-05
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles de...Gravatar herbelin2001-09-19
* Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ...Gravatar herbelin2001-09-10
* Nettoyage reduce_to_ind et one_step_reduceGravatar herbelin2001-09-09
* ParsingGravatar herbelin2001-08-10
* Elimination des coupures quand les 'clause' se réduisent à des hypothèses,...Gravatar herbelin2001-08-05
* Pretty -> PrettypGravatar filliatr2001-05-28
* amelioration de la structure des universGravatar barras2001-03-28
* entetesGravatar filliatr2001-03-15
* application patch Cuit Alvarado : tclTHENSi et intros_until_n exportésGravatar filliatr2001-02-01
* Prise en compte des let-in dans les fonctions de réduction pour les tactiquesGravatar herbelin2000-11-27
* correction Abstract (et make world passe!)Gravatar filliatr2000-11-02
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Renommage canonique :Gravatar herbelin2000-10-18
* Renommage AppL en AppGravatar herbelin2000-10-01