aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/refine.ml
Commit message (Expand)AuthorAge
...
* 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-07-01 02:26:21 +0000