aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/inductive.ml
Commit message (Expand)AuthorAge
* Auto,Dhyp,Elim / Reduction de Evar / declarations eliminationsGravatar filliatr1999-11-24
* module WcclausenvGravatar filliatr1999-11-22
* module Tactics (debut)Gravatar filliatr1999-11-22
* module Pattern, Wcclausenv (interface) et TacticalsGravatar filliatr1999-11-19
* ensembles de contraintes d'universGravatar filliatr1999-09-25
* suppression champs inutiles dans constantes et inductifs; verification defini...Gravatar filliatr1999-08-27
* environnement surGravatar filliatr1999-08-26
* modules Instantiate, Constant et InductiveGravatar filliatr1999-08-25