aboutsummaryrefslogtreecommitdiff
path: root/tactics/refine.ml
AgeCommit message (Expand)Author
2003-10-13Deplacement next_global_ident_away dans Termopsherbelin
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
2002-12-09Ajout Simpl et Change sur des sous-termesherbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2002-04-02- modifs de la condition de garde pour mieux tenir compte des raisonnementsbarras
2002-03-27Simplification de Proof_type.prim_ruleherbelin
2002-02-15petits changements cosmetiques sur les tactiquesbarras
2001-12-18coq-bugs #12: probleme de metamap resolubarras
2001-12-13compat ocaml 3.03filliatr
2001-11-05GROS COMMIT:barras
2001-09-20let-in dans Refinefilliatr
2001-06-25Refine sur les CoFixfilliatr
2001-05-25Remplacement push_rec_types (Rel) pour Fix parpush_named_rec_typesherbelin
2001-05-03Changement de la structure des points fixesbarras
2001-03-28amelioration de la structure des universbarras
2001-03-15entetesfilliatr
2001-03-09bug de refine: uncaught exception Array.subbarras
2001-03-01nouvelle implantation de la reductionbarras
2000-12-15suppression warning et calcule type dans replace_by_meta dans tous les casfilliatr
2000-11-02suppression des (* open Generic *)filliatr
2000-10-18Simplifications autour de typed_type (renommé types par analogie avec sorts)...herbelin
2000-10-18Renommage canonique :herbelin
2000-10-03mise en pageherbelin
2000-10-01Renommage AppL en Appherbelin
2000-09-26Nettoyage pretyping; ise_resolve_* devient understand_*; Ajout d'une notion d...herbelin
2000-09-14Abstraction de constrherbelin
2000-09-12Modification mkAppL; abstraction via kind_of_term; changement dans Reductionherbelin
2000-09-10Correction pour make docherbelin
2000-09-10Suppression de Abstherbelin
2000-09-10Ajout d'un LetIn primitif.herbelin
2000-08-28cosmétiqueherbelin
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclarationsherbelin
2000-07-20portage Refinefilliatr