aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/indrec.ml
Commit message (Expand)AuthorAge
...
* Paramétrisation vis à vis de existential_keyGravatar herbelin2003-09-06
* Nouvelle mouture du traducteur v7->v8Gravatar herbelin2003-08-11
* simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...Gravatar letouzey2003-04-16
* *** empty log message ***Gravatar barras2003-03-12
* Bug en présence de let-inGravatar herbelin2003-01-15
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Intégration des modifs de la branche mowgli :Gravatar herbelin2002-11-05
* Un peu (plus) d'ordre dans Nametab...Gravatar coq2002-09-24
* Renoncement à distinguer les types "constr" et "types"; nettoyageGravatar herbelin2002-08-13
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* - Reforme de la gestion des args recursifs (via arbres reguliers)Gravatar barras2002-02-14
* petit nettoyage de kernel/inductiveGravatar barras2002-02-07
* changement generation de schema d'elimination, False_rec est primitif, Constr...Gravatar mohring2002-01-31
* code mortGravatar herbelin2002-01-24
* warning en mode verbeux seulementGravatar filliatr2002-01-21
* Amélioration affichage échec lookup_eliminatorGravatar herbelin2002-01-17
* compat ocaml 3.03Gravatar filliatr2001-12-13
* GROS COMMIT:Gravatar barras2001-11-05