aboutsummaryrefslogtreecommitdiff
path: root/kernel/inductive.ml
AgeCommit message (Expand)Author
2000-03-08Peaufinement nouveaux types inductive_summary et constructor_summary en vueherbelin
1999-12-15Nouveaux types 'constructor' et 'inductive' dans Term;herbelin
1999-12-10debug discharge et inductifsfilliatr
1999-12-09Ajout des messages d'erreurs de Casesherbelin
1999-12-07debuggage inductifs (suite) / compilation Dhyp et Auto (mais pas linkesfilliatr
1999-12-06declarations eliminations / debuggae inductifs (debut)filliatr
1999-12-05explicitations erreurs inductifsfilliatr
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 15:30:46 +0000