aboutsummaryrefslogtreecommitdiff
path: root/library/indrec.ml
AgeCommit message (Expand)Author
2000-10-01Chasse aux de-cast inutilesherbelin
2000-09-15On laisse les LetIn dans les types des constructeurs et des éliminationsherbelin
2000-09-14Abstraction de constrherbelin
2000-09-12Modification mkAppL; abstraction via kind_of_term; changement dans Reductionherbelin
2000-09-10Correction pour make docherbelin
2000-09-10Suppression de Abstherbelin
2000-09-10Ajout d'un LetIn primitif.herbelin
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclarationsherbelin
2000-07-01Précalcul de la forme canonique des constructeurs et arités pour traiter le...herbelin
2000-06-01Mise en place d'un choix constr/typed_type en remplacement de certains Castherbelin
2000-05-31Nettoyage de Genericherbelin
2000-05-22Bugs d'index d'inductiveherbelin
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-18Adaptation pour nouveaux inductifs (cf Inductive)herbelin
2000-05-04Renommage try_mutind_of en find_inductive (on fait ce qu'on peut !)herbelin
2000-03-21Nettoyageherbelin
2000-03-21Prise en compte nouveau case_infoherbelin
2000-01-07Correction pbs liés aux evarherbelin
1999-12-15Nouveaux types 'constructor' et 'inductive' dans Term;herbelin
1999-11-26Déplacement fonction transform_rec vers pretypingherbelin
1999-11-23modules Indrec, Tacentries, Hiddentacfilliatr
1999-11-22modules Indrec, Wcclausenv; progression dans Tacticalsfilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 10:43:47 +0000