aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2008-06-06ajout d'un printer pour les contraintes d'univers + correction d'un bug sur l...soubiran
2008-05-27Correction du problème de complexité de Print Assumptions :aspiwack
2008-05-21refined the conversion oraclebarras
2008-05-15really fixed Georges\' bugbarras
2008-05-14corrige le bug de Georgesbarras
2008-05-12Changement de stratégie vis à vis du commit 10859 sur la gestion desherbelin
2008-05-11- Cleanup parsing of binders, reducing to a single production for allmsozeau
2008-04-30Réutilisation de l'infrastructure pour le polymorphisme d'univers desherbelin
2008-04-27Correction du bug des types singletons pas sous-type de Setherbelin
2008-04-25correction bug 1839soubiran
2008-04-23Prise en compte des coercions dans les clauses "with" même si le typeherbelin
2008-04-23correction d'un bug sur la compostion des substitutions induites par les alia...soubiran
2008-04-23correction du bug sur Parameter Inline que j'ai reouvert hier par inadvertancesoubiran
2008-04-22correction bug 1839soubiran
2008-04-22fixed universes bug related to module inclusionbarras
2008-04-21added the .vo checker (with independent Makefile)barras
2008-04-21- Parameterize unification by two sets of transparent_state, one for openmsozeau
2008-04-21Correction bug 1838 + doc modules.soubiran
2008-04-20Add the ability to give a transparent_state for conversion, tomsozeau
2008-04-14suite 10790 (identificateurs)herbelin
2008-04-13Bugs, nettoyage, et améliorations diversesherbelin
2008-04-03Patch sur le typage d'un foncteur applique a un alias.soubiran
2008-04-01Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientherbelin
2008-03-28- Second pass on implementation of let pattern. Parse "let ' par [as x]?msozeau
2008-03-26Correction d'un bug sur Import/Export : ces fonctionnalites sont gerees en-de...soubiran
2008-03-25Correction de bugs relatifs a la compostion des substitutionssoubiran
2008-03-18improved the implementation of rtreebarras
2008-03-18git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10690 85f007b7-540e-0...barras
2008-03-15Application de refresh_universes dans typing.ml et retyping.ml : lesherbelin
2008-03-14Ajout des alias de module dans le noyau.soubiran
2008-03-10fold travaille maintenant sur la forme beta-iota-zeta réduite duherbelin
2008-03-09Fix a few bugs in Program: use user-given typing constraints formsozeau
2008-03-05Attempt of fix for extraction of modules typesletouzey
2008-02-27patch for C code of addmuldiv31thery
2008-02-22Merge with lmamane's private branch:lmamane
2008-02-15Patch bug #1799soubiran
2008-02-08Add more information to IllFormedRecBody exceptions, to show the exactmsozeau
2008-02-01Beaoucoup de changements dans la representation interne des modules.soubiran
2008-01-31Finish let| implementation and document itmsozeau
2008-01-18bug in accessing n-th abstractionbarras
2008-01-05Fixed bug 1761 (unexpected anomaly when constructor type has invalidherbelin
2007-12-31Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...msozeau
2007-12-18Nettoyage de code en vue de la release. Plus de Warning: Unused aspiwack
2007-12-05Factorisation des opérations sur le type option de Util dans un module aspiwack
2007-11-09Nettoyage de Print Assumptions :aspiwack
2007-11-07bug in infos_and_sort: type of constructor was not reduced enoughbarras
2007-10-30bug in safe_typing: univ constraints generated by section variables were not ...barras
2007-10-04Correction bug 1718 (lazy delta unfolding used to miss delta on rels and vars)herbelin
2007-09-30Ajout infos de débogage de "universe inconsistency" quand option Setherbelin
2007-09-15* Adding compability with ocaml 3.10 + camlp5 (rework of letouzey