aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/indrec.ml
Commit message (Expand)AuthorAge
* Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...Gravatar herbelin2005-12-17
* Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...Gravatar herbelin2005-12-17
* Changement des named_contextGravatar gregoire2005-12-02
* parametres inductifsGravatar mohring2005-11-28
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* Types inductifs parametriquesGravatar mohring2005-11-02
* Standardisation of function names about global references (especially, renami...Gravatar herbelin2005-02-18
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
* Expansion du prédicat du 'match' vis à vis de la dépendance en le terme fi...Gravatar herbelin2004-08-24
* Nouvelle en-têteGravatar herbelin2004-07-16
* Eta-expansion du predicat dans build_indrec (suite)Gravatar herbelin2004-07-11
* Eta-expansion du predicat pas seulement pour make_case mais aussi pour build_...Gravatar herbelin2004-07-11
* Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in...Gravatar herbelin2003-09-12
* Ajout construction If primitive dans constr_expr et rawconstrGravatar herbelin2003-09-09
* 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