aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/inv.ml
Commit message (Expand)AuthorAge
* 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
* petit nettoyage de kernel/inductiveGravatar barras2002-02-07
* Ajout tactiques Rename et Pose; modifications pour InversionGravatar herbelin2002-02-01
* Remplacement cut_intro par true_cut_anonGravatar herbelin2002-01-24
* Bug dépendances en les corps des let-in oubliéesGravatar herbelin2002-01-24
* compat ocaml 3.03Gravatar filliatr2001-12-13
* nouvel algo de conversion plus uniformeGravatar barras2001-11-29
* GROS COMMIT:Gravatar barras2001-11-05
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* ParsingGravatar herbelin2001-08-10
* Remplacement de 'clause' par 'hyps' pour les tactiques qui ne peuvent pas s'a...Gravatar herbelin2001-08-05
* Branchement sur bad_tactic_argsGravatar herbelin2001-07-10
* amelioration de la structure des universGravatar barras2001-03-28
* entetesGravatar filliatr2001-03-15
* Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...Gravatar herbelin2001-02-14