aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/refine.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 2110 (tactic "refine" was calling (co)mutual_fix with index 0Gravatar herbelin2009-06-06
* ## Lines starting with '## ' will be removed from the log message.Gravatar msozeau2009-06-01
* - Fixing bug #2084 (unification not checking sort constraints), hopingGravatar herbelin2009-04-08
* Cleaning/uniformizing the interface of tacticals.mliGravatar herbelin2009-03-14
* About "apply in":Gravatar herbelin2008-12-09
* Adaptation to ocaml 3.11 new semantics of String.index_from (see bug #1974)Gravatar herbelin2008-11-04
* Optimisation de clenv.ml pour que meta_instance ne soit pas appeléGravatar herbelin2008-10-18
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* Backtrack sur l'effacement dans le contexte de but des lieursGravatar herbelin2007-05-19
* Wish #1582 (3eme)Gravatar herbelin2007-05-18
* Quelques essais autour du wish implicite au rapport de bug #1582 (2eme)Gravatar herbelin2007-05-18
* Quelques essais autour du wish implicite au rapport de bug #1582Gravatar herbelin2007-05-18
* Correction d'un bug refineGravatar herbelin2006-11-10
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
* Changement des named_contextGravatar gregoire2005-12-02
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* Fix bug #931: leave dependent evars as such for refineGravatar herbelin2005-03-08
* Restauration type casted_open_constr pour tactique refine car l'unification n...Gravatar herbelin2004-12-09
* Garder les cast semble décidément le meilleur moyen de rester synchrone ave...Gravatar herbelin2004-12-06
* Suppression des cast après avoir utiliser l'information de type (Tacinv envo...Gravatar herbelin2004-12-06
* Déplacement de la coercion vis à vis du but au niveau de Refine suite à ch...Gravatar herbelin2004-12-06
* Réparation bug #888 (les tactiques fix et cofix exigent autant de sous-buts ...Gravatar herbelin2004-12-06
* inclusion de meta_map dans evar_defsGravatar barras2004-09-12
* Nouvelle en-têteGravatar herbelin2004-07-16
* bug #787 de RolandGravatar barras2004-06-02
* Correction bug soumis par YvesGravatar herbelin2003-12-13
* Deplacement next_global_ident_away dans TermopsGravatar herbelin2003-10-13
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* Ajout Simpl et Change sur des sous-termesGravatar herbelin2002-12-09
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* - modifs de la condition de garde pour mieux tenir compte des raisonnementsGravatar barras2002-04-02
* Simplification de Proof_type.prim_ruleGravatar herbelin2002-03-27
* petits changements cosmetiques sur les tactiquesGravatar barras2002-02-15
* coq-bugs #12: probleme de metamap resoluGravatar barras2001-12-18
* compat ocaml 3.03Gravatar filliatr2001-12-13
* GROS COMMIT:Gravatar barras2001-11-05
* let-in dans RefineGravatar filliatr2001-09-20
* Refine sur les CoFixGravatar filliatr2001-06-25
* Remplacement push_rec_types (Rel) pour Fix parpush_named_rec_typesGravatar herbelin2001-05-25
* Changement de la structure des points fixesGravatar barras2001-05-03
* amelioration de la structure des universGravatar barras2001-03-28
* entetesGravatar filliatr2001-03-15
* bug de refine: uncaught exception Array.subGravatar barras2001-03-09
* nouvelle implantation de la reductionGravatar barras2001-03-01
* suppression warning et calcule type dans replace_by_meta dans tous les casGravatar filliatr2000-12-15
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Renommage canonique :Gravatar herbelin2000-10-18
* mise en pageGravatar herbelin2000-10-03