aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
* suite 10790 (identificateurs)Gravatar herbelin2008-04-14
* Bugs, nettoyage, et améliorations diversesGravatar herbelin2008-04-13
* Patch sur le typage d'un foncteur applique a un alias.Gravatar soubiran2008-04-03
* Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientGravatar herbelin2008-04-01
* - Second pass on implementation of let pattern. Parse "let ' par [as x]?Gravatar msozeau2008-03-28
* Correction d'un bug sur Import/Export : ces fonctionnalites sont gerees en-de...Gravatar soubiran2008-03-26
* Correction de bugs relatifs a la compostion des substitutionsGravatar soubiran2008-03-25
* improved the implementation of rtreeGravatar barras2008-03-18
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10690 85f007b7-540e-0...Gravatar barras2008-03-18
* Application de refresh_universes dans typing.ml et retyping.ml : lesGravatar herbelin2008-03-15
* Ajout des alias de module dans le noyau.Gravatar soubiran2008-03-14
* fold travaille maintenant sur la forme beta-iota-zeta réduite duGravatar herbelin2008-03-10
* Fix a few bugs in Program: use user-given typing constraints forGravatar msozeau2008-03-09
* Attempt of fix for extraction of modules typesGravatar letouzey2008-03-05
* patch for C code of addmuldiv31Gravatar thery2008-02-27
* Merge with lmamane's private branch:Gravatar lmamane2008-02-22
* Patch bug #1799Gravatar soubiran2008-02-15
* Add more information to IllFormedRecBody exceptions, to show the exactGravatar msozeau2008-02-08
* Beaoucoup de changements dans la representation interne des modules.Gravatar soubiran2008-02-01
* Finish let| implementation and document itGravatar msozeau2008-01-31
* bug in accessing n-th abstractionGravatar barras2008-01-18
* Fixed bug 1761 (unexpected anomaly when constructor type has invalidGravatar herbelin2008-01-05
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31
* Nettoyage de code en vue de la release. Plus de Warning: Unused Gravatar aspiwack2007-12-18
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
* Nettoyage de Print Assumptions :Gravatar aspiwack2007-11-09
* bug in infos_and_sort: type of constructor was not reduced enoughGravatar barras2007-11-07
* bug in safe_typing: univ constraints generated by section variables were not ...Gravatar barras2007-10-30
* Correction bug 1718 (lazy delta unfolding used to miss delta on rels and vars)Gravatar herbelin2007-10-04
* Ajout infos de débogage de "universe inconsistency" quand option SetGravatar herbelin2007-09-30
* * 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