aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacticals.ml
Commit message (Expand)AuthorAge
* 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
* Modification mkAppL; abstraction via kind_of_term; changement dans ReductionGravatar herbelin2000-09-12
* Correction pour make docGravatar herbelin2000-09-10
* Suppression de AbstGravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* Modifs d'interpretation de patternsGravatar delahaye2000-07-21
* Suite restructuration inductifs; changement nom module Constant en DeclarationsGravatar herbelin2000-05-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-16 09:40:58 +0000