aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/indrec.ml
Commit message (Expand)AuthorAge
* prise en compte des défs locales dans les arguments des inductifs; meilleure...Gravatar herbelin2001-02-14
* Reparation bug mutuels indGravatar mohring2000-11-22
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Prise en compte de Let dans build_dependent_inductiveGravatar herbelin2000-10-11
* Renommage AppL en AppGravatar herbelin2000-10-01
* Chasse aux de-cast inutilesGravatar herbelin2000-10-01
* On laisse les LetIn dans les types des constructeurs et des éliminationsGravatar herbelin2000-09-15
* Abstraction de constrGravatar herbelin2000-09-14
* Modification mkAppL; abstraction via kind_of_term; changement dans ReductionGravatar herbelin2000-09-12
* Correction pour make docGravatar herbelin2000-09-10
* Suppression de AbstGravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* Précalcul de la forme canonique des constructeurs et arités pour traiter le...Gravatar herbelin2000-07-01
* Mise en place d'un choix constr/typed_type en remplacement de certains CastGravatar herbelin2000-06-01
* Nettoyage de GenericGravatar herbelin2000-05-31
* Bugs d'index d'inductiveGravatar herbelin2000-05-22
* suppression de l'env/sigma dans les fonctions de reduction beta et iota seulsGravatar herbelin2000-05-22
* Suite restructuration inductifs; changement nom module Constant en DeclarationsGravatar herbelin2000-05-22
* Adaptation pour nouveaux inductifs (cf Inductive)Gravatar herbelin2000-05-18
* Renommage try_mutind_of en find_inductive (on fait ce qu'on peut !)Gravatar herbelin2000-05-04
* NettoyageGravatar herbelin2000-03-21
* Prise en compte nouveau case_infoGravatar herbelin2000-03-21
* Correction pbs liés aux evarGravatar herbelin2000-01-07
* Nouveaux types 'constructor' et 'inductive' dans Term;Gravatar herbelin1999-12-15
* Déplacement fonction transform_rec vers pretypingGravatar herbelin1999-11-26
* modules Indrec, Tacentries, HiddentacGravatar filliatr1999-11-23
* modules Indrec, Wcclausenv; progression dans TacticalsGravatar filliatr1999-11-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-21 09:50:37 +0000