aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
* added isProd to term.mli.Gravatar coq2006-02-16
* Variable inutiliséeGravatar herbelin2006-01-21
* *** empty log message ***Gravatar barras2006-01-20
* Suppression résidus code v7 et traducteurGravatar herbelin2006-01-11
* Ajout de la longueur de l'arité des constructeurs dans one_inductive_body et...Gravatar herbelin2006-01-10
* Détection var inutile par ocaml 3.09Gravatar herbelin2006-01-10
* Uniformisation: extension de la suppression d'un casts dans collapse_app à l...Gravatar herbelin2005-12-21
* Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...Gravatar herbelin2005-12-17
* Orthographe de 'instantiate'Gravatar herbelin2005-12-17
* j'avais oublie ces deux fichiers.Gravatar gregoire2005-12-06
* correction bug 881.Gravatar gregoire2005-12-05
* changement d'egalite pour le named_context_valGravatar gregoire2005-12-05
* Changement des named_contextGravatar gregoire2005-12-02
* parametres inductifsGravatar mohring2005-11-28
* bug #909: Top n'est cree que si le contexte est videGravatar barras2005-11-23
* petites corrections + contournement bug projectionsGravatar barras2005-11-18
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* Nettoyage suite nouveaux avertissements Y et Z de ocaml 3.09Gravatar herbelin2005-11-08
* Nettoyage suite nouvel avertissement Z de ocaml 3.09Gravatar herbelin2005-11-08
* Types inductifs parametriquesGravatar mohring2005-11-02
* Suppression code inactif et commentaire apparemment incorrect (pour éviter c...Gravatar herbelin2005-09-09
* Simplification message d'anomalieGravatar herbelin2005-09-08
* argument inutilisé de zip: toujours l'identitéGravatar letouzey2005-08-22
* Sur le conseil de X.Leroy: x=[||] devient Array.length x=0Gravatar letouzey2005-08-19
* Utilisation de la non-équivalence d'inductifs pour le case_info (cf message ...Gravatar herbelin2005-07-21
* reactivation de l optim des fermeturesGravatar barras2005-07-13
* backtrack modif de knh...Gravatar barras2005-07-13
* *** empty log message ***Gravatar barras2005-07-13
* test du tag de reductionGravatar barras2005-07-12
* Correction bug #983Gravatar herbelin2005-06-28
* Bug fix for a bug reported by Roland: the function that detects the constantsGravatar sacerdot2005-05-23
* Bug affichage graphe universGravatar herbelin2005-05-05
* Code v7 obsoleteGravatar herbelin2005-05-05
* MAJ commentaires et inversion du sens du graphe de contraintes pour extensibi...Gravatar herbelin2005-05-05
* Moving centralised discharge into dispatched discharge_function; required to ...Gravatar herbelin2005-02-18
* Added map_named_contextGravatar herbelin2005-02-18
* Moved Indmap and ConstrMap from Libnames to Names for use in CookingGravatar herbelin2005-02-18
* Uniformisation de destApplication en destAppGravatar herbelin2005-02-12
* Uniformisation de destApplication en destApp; simplification decompose_appGravatar herbelin2005-02-12
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* 1. added code to handle the inclusion of inductive types and constructors inGravatar sacerdot2005-01-17
* Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changedGravatar sacerdot2005-01-14
* Construct "T with (Definition|Module) id := c" generalized toGravatar sacerdot2005-01-13
* [ Waiting for a keyword to control expansion during functor application ]Gravatar sacerdot2005-01-05
* HUGE COMMITGravatar sacerdot2005-01-03
* * added subst_evaluable_referenceGravatar sacerdot2004-12-07
* CommentaireGravatar herbelin2004-12-06
* *** empty log message ***Gravatar gregoire2004-11-29
* Code mortGravatar herbelin2004-11-22