aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/inductive.ml
Commit message (Expand)AuthorAge
* Nouveaux types 'constructor' et 'inductive' dans Term;Gravatar herbelin1999-12-15
* debug discharge et inductifsGravatar filliatr1999-12-10
* Ajout des messages d'erreurs de CasesGravatar herbelin1999-12-09
* debuggage inductifs (suite) / compilation Dhyp et Auto (mais pas linkesGravatar filliatr1999-12-07
* declarations eliminations / debuggae inductifs (debut)Gravatar filliatr1999-12-06
* explicitations erreurs inductifsGravatar filliatr1999-12-05
* Modification pour faire compiler pretyping.ml qui maintenant compileGravatar herbelin1999-11-26
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-31 04:37:35 +0000