aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
* * Adding compability with ocaml 3.10 + camlp5 (rework of Gravatar letouzey2007-09-15
* Suppression des type_app et body_of_type qui alourdissent inutilement le codeGravatar herbelin2007-08-27
* normalisation (by closure) was not performed under fixpointsGravatar barras2007-07-12
* kill an ugly warning about a non-exhaustive patternGravatar letouzey2007-06-26
* Correction de plusieurs bugs de l'export XML (utilisation d'un type deGravatar herbelin2007-06-21
* ajout de head0 et tail0 en natifGravatar bgregoir2007-06-20
* Corrections dans le Print Assumption. Les definitions locales ("Let") Gravatar aspiwack2007-05-30
* Memory optimisation for modules and constrs substitutions.Gravatar soubiran2007-05-30
* Correction of (PR#1576).Gravatar soubiran2007-05-25
* Suite restructuration unification et division des problèmesGravatar herbelin2007-05-23
* Nettoyage et standardisation des messages d'erreurs.Gravatar herbelin2007-05-17
* corrections bug dans l'implem de int31Gravatar bgregoir2007-05-15
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11
* New keyword "Inline" for Parameters and Axioms for automatic Gravatar soubiran2007-04-25
* Correction partielle du bug #1388 (augmentation de la taille des code accepte...Gravatar jforest2007-04-05
* Modification de la vm:Gravatar notin2007-03-27
* Suppression argument pattern_source du case_info (code jamais utilisé)Gravatar herbelin2007-03-15
* Removed some useless code in mod_typing that was redundant with safe_typing.Gravatar soubiran2007-02-21
* Fixed the pseudo-cicularity problem due to the with operator on Module Type.Gravatar soubiran2007-02-21
* Suppresion de la catégorie des inductifs singletons larges dontGravatar herbelin2007-02-09
* Suppression de code mortGravatar notin2007-02-01
* suite du commit 9557 Gravatar soubiran2007-01-30
* Petite correction sur un message d'erreur renvoyé au sous typage.Gravatar soubiran2007-01-30
* modifications des messages d'erreurs renvoyés lors de la comparaison Gravatar soubiran2007-01-24
* Correction du bug #1315:Gravatar notin2007-01-22
* Prise en compte des univers algébriques dans les types inférés dansGravatar herbelin2007-01-19
* Protection contre les warnings 'unused variable' de ocaml 3.09Gravatar herbelin2007-01-19
* Correction bug #1302Gravatar herbelin2007-01-17
* Correction du bug #1273 (problème avec les paramètres non récursivement un...Gravatar notin2006-12-12
* cosmetiqueGravatar barras2006-12-12
* Changement dans le kernel : Gravatar bgregoir2006-12-11
* bug condition de gardeGravatar barras2006-12-08
* Débranchement du polymorphisme de sorte sur les définitions dans TypeGravatar herbelin2006-10-30
* dependencesGravatar barras2006-10-30
* Compatibilité du polymorphisme de constantes avec les sections.Gravatar herbelin2006-10-29
* Extension du polymorphisme de sorte au cas des définitions dans Type.Gravatar herbelin2006-10-28
* Ajout fold_rel_declaration et fold_named_declarationGravatar herbelin2006-10-27
* Correction de 2 bugs critiques du polymorphisme d'universGravatar herbelin2006-10-27
* changement des _sym par _comm dans setoid_ringGravatar bgregoir2006-10-27
* Clarification des contraintes sur le contexte de paramètres desGravatar herbelin2006-10-17
* Protection raise en début de séquence (en attendant que le code caché trou...Gravatar herbelin2006-10-12
* Déplacement de on_judgment_type de Typeops vers TermopsGravatar herbelin2006-10-06
* Correction de deux cas où les types inductifs n'étaient pas comparésGravatar herbelin2006-10-05
* Changement de comportement du [rewrite ... in H]: Coq échoue si HGravatar notin2006-10-03
* Correction du bug #1181Gravatar jforest2006-09-14
* Indentation + typoGravatar notin2006-09-01
* Ajout iter_rel_context/iter_named_contextGravatar herbelin2006-09-01
* Appel à caml_modify pour Ocaml 3.07Gravatar notin2006-09-01
* Export de closedn pour EvarutilGravatar herbelin2006-08-28
* correction bug vm_computeGravatar bgregoir2006-08-25