aboutsummaryrefslogtreecommitdiff
path: root/kernel/inductive.mli
AgeCommit message (Expand)Author
2000-05-22suppression de l'env/sigma dans les fonctions de reduction beta et iota seulsherbelin
2000-05-22Suite restructuration inductifs; changement nom module Constant en Declarationsherbelin
2000-05-18Restructuration des outils pour les inductifs.herbelin
2000-05-16Ajout mis_typepathherbelin
2000-04-27Retrait fullmind de inductive_summary pour simplicitéherbelin
2000-04-20Abstraction du type typed_type (un pas vers les jugements 2 niveaux)herbelin
2000-03-21Ajout des fonctions de formation du 'case_info'; Suppression de make_arity et...herbelin
2000-03-08Peaufinement nouveaux types inductive_summary et constructor_summary en vueherbelin
2000-01-28documentationfilliatr
2000-01-27erreurs latex dans interfacesfilliatr
1999-12-15Nouveaux types 'constructor' et 'inductive' dans Term;herbelin
1999-12-09Ajout des messages d'erreurs de Casesherbelin
1999-12-05explicitations erreurs inductifsfilliatr
1999-11-24Auto,Dhyp,Elim / Reduction de Evar / declarations eliminationsfilliatr
1999-11-23modules Indrec, Tacentries, Hiddentacfilliatr
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-09-19 - un effort sur la doc (ocamlweb)filliatr
1999-08-30un petit effort de presentation dans les interfacesfilliatr
1999-08-27suppression champs inutiles dans constantes et inductifs; verification defini...filliatr
1999-08-26environnement surfilliatr
1999-08-25modules Instantiate, Constant et Inductivefilliatr
1999-08-24mach et himsg; typage sans extractionfilliatr
1999-08-18module Reduction (fin)filliatr
1999-08-17module Closurefilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 10:03:09 +0000