aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/refine.ml
Commit message (Expand)AuthorAge
* 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
* Renommage AppL en AppGravatar herbelin2000-10-01
* Nettoyage pretyping; ise_resolve_* devient understand_*; Ajout d'une notion d...Gravatar herbelin2000-09-26
* Abstraction de constrGravatar herbelin2000-09-14
* 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
* cosmétiqueGravatar herbelin2000-08-28
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* portage RefineGravatar filliatr2000-07-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 17:27:11 +0000