aboutsummaryrefslogtreecommitdiff
path: root/kernel/inductive.ml
AgeCommit message (Expand)Author
1999-11-26Modification pour faire compiler pretyping.ml qui maintenant compileherbelin
1999-11-24Auto,Dhyp,Elim / Reduction de Evar / declarations eliminationsfilliatr
1999-11-22module Wcclausenvfilliatr
1999-11-22module Tactics (debut)filliatr
1999-11-19module Pattern, Wcclausenv (interface) et Tacticalsfilliatr
1999-09-25ensembles de contraintes d'universfilliatr
1999-08-27suppression champs inutiles dans constantes et inductifs; verification defini...filliatr
1999-08-26environnement surfilliatr
1999-08-25modules Instantiate, Constant et Inductivefilliatr