aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/inv.ml
Commit message (Expand)AuthorAge
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* - Added two new introduction patterns with the following temptative syntaxes:Gravatar herbelin2009-06-07
* Cleaning/uniformizing the interface of tacticals.mliGravatar herbelin2009-03-14
* - Deactivation of dynamic loading on Mac OS 10.5 (see bug #2024).Gravatar herbelin2009-01-11
* Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->Gravatar herbelin2008-12-31
* About "apply in":Gravatar herbelin2008-12-09
* - Fixed bug 1968 (inversion failing due to a Not_found bug introduced inGravatar herbelin2008-11-09
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* 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
* - Un peu de doc, préparation du CHANGES pour la release.Gravatar herbelin2008-04-15
* Bugs, nettoyage, et améliorations diversesGravatar herbelin2008-04-13
* Quelques améliorations des intro patterns:Gravatar herbelin2008-04-04
* bug in accessing n-th abstractionGravatar barras2008-01-18
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
* Ajout de eelim, ecase, edestruct et einduction (expérimental).Gravatar herbelin2007-10-03
* New intro pattern "@A", which generates a fresh name based on A.Gravatar glondu2007-07-06
* 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 motif d'introduction "?" (IntroAnonymous) pour laisser CoqGravatar herbelin2006-01-16
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* Réparation bug #1004; nettoyageGravatar herbelin2005-09-08
* Correction bug de dependent_hyps qui ne met pas à jour le type des hyps dép...Gravatar herbelin2005-03-20
* Restructuration fonctions de réécriture depuis égalité dépendanteGravatar herbelin2004-10-27
* Simplifications concommitantes à la correction du bug #855Gravatar herbelin2004-09-24
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
* inclusion de meta_map dans evar_defsGravatar barras2004-09-12
* 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
* bugs avec Pose et AssertGravatar barras2004-01-09
* factorisation et generalisation des clausesGravatar barras2003-11-13
* Un Try supplementaire utile pour la compatibilite, car bring_hyps dans genera...Gravatar herbelin2003-10-13
* Bug calcul du nom de la premiere equationGravatar herbelin2003-10-11
* Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'Gravatar herbelin2003-10-10
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* nouveau Subst:Gravatar barras2002-12-17
* Repercussion de la possibilit de mettre des hyps quantifiees dans Simplify_eq...Gravatar herbelin2002-06-05
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* *** empty log message ***Gravatar barras2002-03-05
* suppression de pop_namedGravatar barras2002-02-22
* petits changements cosmetiques sur les tactiquesGravatar barras2002-02-15
* mauvais comportement de l'inversion vis-a-vis des letsGravatar barras2002-02-08