aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proof_type.ml
Commit message (Expand)AuthorAge
* Suppression des stamps et donc des *_constraintsGravatar clrenard2001-11-12
* Suite de la suppression : enamed_declaration est remplace par evar_map.Gravatar clrenard2001-11-06
* Suppression des local_constraints, des ctxtty et du focus.Gravatar clrenard2001-11-06
* GROS COMMIT:Gravatar barras2001-11-05
* Nouvelle tactique primitive ThinBody et nouvelles tactiques utilisateurs 'Cle...Gravatar herbelin2001-10-05
* Ajout tactique TrueCut qui fait la coupure du calcul des séquents; nouvelle ...Gravatar herbelin2001-08-07
* Les réduction dans les hypothèses s'appliquent maintenant au corps de la dÃ...Gravatar herbelin2001-06-25
* Ajout de _ dans les patterns d'introGravatar mohring2001-04-12
* amelioration de la structure des universGravatar barras2001-03-28
* entetesGravatar filliatr2001-03-15
* Déplacement de qualid dans Nametab, hors du noyauGravatar herbelin2001-03-01
* Prise en compte noms longs dans SuperAutoGravatar herbelin2001-02-16
* Portage d'AutoRewriteGravatar delahaye2000-12-02
* Renommage canonique :Gravatar herbelin2000-10-18
* Nettoyage pretyping; ise_resolve_* devient understand_*; Ajout d'une notion d...Gravatar herbelin2000-09-26
* Pattern matching de sous-termesGravatar delahaye2000-08-17
* Modifs de presentation.Gravatar delahaye2000-06-28
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 15:59:21 +0000