aboutsummaryrefslogtreecommitdiff
path: root/pretyping/indrec.ml
AgeCommit message (Expand)Author
2003-09-12Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in...herbelin
2003-09-09Ajout construction If primitive dans constr_expr et rawconstrherbelin
2003-09-06Paramétrisation vis à vis de existential_keyherbelin
2003-08-11Nouvelle mouture du traducteur v7->v8herbelin
2003-04-16simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...letouzey
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