aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/elim.ml
Commit message (Expand)AuthorAge
* print_id, print_sp -> pr_id, pr_spGravatar herbelin2000-11-23
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Suppression du test de convertibilite inutile pour la plupart des exact; 2 ve...Gravatar herbelin2000-10-13
* Abstraction de constrGravatar herbelin2000-09-14
* Correction pour make docGravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Changement nommage des hypothèsesGravatar herbelin2000-05-22
* Retour comportement de la version précédenteGravatar herbelin2000-05-22
* Effets de bords suite à la restructuration des inductives (cf Inductive)Gravatar herbelin2000-05-18
* Retrait du i pour tclTHEN_i et correction bugs DecomposeGravatar herbelin2000-05-16
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* Déplacement du type reference dans TermGravatar herbelin2000-04-28
* Nettoyage de l'interface d'Astterm; renommage des {pf_,}constr_of_com* en {pf...Gravatar herbelin2000-03-28
* - Typing -> Safe_typingGravatar filliatr1999-12-01
* Auto,Dhyp,Elim / Reduction de Evar / declarations eliminationsGravatar filliatr1999-11-24
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-16 22:18:35 +0000