aboutsummaryrefslogtreecommitdiff
path: root/pretyping/indrec.ml
AgeCommit message (Expand)Author
2003-03-12*** empty log message ***barras
2003-01-15Bug en présence de let-inherbelin
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-11-05Intégration des modifs de la branche mowgli :herbelin
2002-09-24Un peu (plus) d'ordre dans Nametab...coq
2002-08-13Renoncement à distinguer les types "constr" et "types"; nettoyageherbelin
2002-08-02Modules dans COQ\!\!\!\!coq
2002-02-14- Reforme de la gestion des args recursifs (via arbres reguliers)barras
2002-02-07petit nettoyage de kernel/inductivebarras
2002-01-31changement generation de schema d'elimination, False_rec est primitif, Constr...mohring
2002-01-24code mortherbelin
2002-01-21warning en mode verbeux seulementfilliatr
2002-01-17Amélioration affichage échec lookup_eliminatorherbelin
2001-12-13compat ocaml 3.03filliatr
2001-11-05GROS COMMIT:barras