aboutsummaryrefslogtreecommitdiff
path: root/proofs/proof_type.mli
AgeCommit message (Expand)Author
2001-11-12Suppression des stamps et donc des *_constraintsclrenard
2001-11-06Suite de la suppression : enamed_declaration est remplace par evar_map.clrenard
2001-11-06Suppression des local_constraints, des ctxtty et du focus.clrenard
2001-11-05GROS COMMIT:barras
2001-10-05Nouvelle tactique primitive ThinBody et nouvelles tactiques utilisateurs 'Cle...herbelin
2001-08-07Ajout tactique TrueCut qui fait la coupure du calcul des séquents; nouvelle ...herbelin
2001-06-25Les réduction dans les hypothèses s'appliquent maintenant au corps de la dÃ...herbelin
2001-04-12Ajout de _ dans les patterns d'intromohring
2001-03-28amelioration de la structure des universbarras
2001-03-15entetesfilliatr
2001-03-01Déplacement de qualid dans Nametab, hors du noyauherbelin
2001-02-16Prise en compte noms longs dans SuperAutoherbelin
2000-12-18Documentationherbelin
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
2000-12-02Portage d'AutoRewritedelahaye
2000-10-18Renommage canonique :herbelin
2000-09-26Nettoyage pretyping; ise_resolve_* devient understand_*; Ajout d'une notion d...herbelin
2000-08-17Pattern matching de sous-termesdelahaye
2000-06-28Modifs de presentation.delahaye
2000-06-21portage EAuto et Ringfilliatr
2000-05-03diverses modifs pour ocamlwebfilliatr
2000-05-03Ajout du langage de tactiquesdelahaye
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:14:55 +0000