aboutsummaryrefslogtreecommitdiff
path: root/library/indrec.ml
AgeCommit message (Expand)Author
2001-11-05GROS COMMIT:barras
2001-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
2001-09-19Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles de...herbelin
2001-09-10Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ...herbelin
2001-05-23amelioration des messages d'erreurs vis a vis des evarsbarras
2001-05-03Changement de la structure des points fixesbarras
2001-03-15entetesfilliatr
2001-02-14prise en compte des défs locales dans les arguments des inductifs; meilleure...herbelin
2000-11-22Reparation bug mutuels indmohring
2000-11-02suppression des (* open Generic *)filliatr
2000-10-18Simplifications autour de typed_type (renommé types par analogie avec sorts)...herbelin
2000-10-11Prise en compte de Let dans build_dependent_inductiveherbelin
2000-10-01Renommage AppL en Appherbelin
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-01 22:51:19 +0000