aboutsummaryrefslogtreecommitdiff
path: root/pretyping/tacred.ml
AgeCommit message (Expand)Author
2000-05-18Effets de bords suite à la restructuration des inductives (cf Inductive)herbelin
2000-03-21Plus besoin de env dans reduce_mind_caseherbelin
2000-01-20Broutillesherbelin
2000-01-13Plus d'unfold inutile des Fix dans Simplherbelin
1999-12-15Nouveaux types 'constructor' et 'inductive' dans Term;herbelin
1999-12-13 - états fabriqués avec -silentfilliatr
1999-12-02modifs pour premiere edition de liensfilliatr