aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
* Bug 2050, commit v8.2 11923-11924 ---> trunkGravatar soubiran2009-02-13
* pushed evar reduction in kernelGravatar barras2009-02-06
* - Deactivation of dynamic loading on Mac OS 10.5 (see bug #2024).Gravatar herbelin2009-01-11
* Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->Gravatar herbelin2008-12-31
* - coq_makefile: target install now respects the original tree structureGravatar herbelin2008-12-24
* fixed kernel bug (de Bruijn) + test-suiteGravatar barras2008-12-02
* Univ: two < instead of a Pervasives.compare on int (as suggested by X. Leroy)Gravatar letouzey2008-11-16
* Correct display of constraints for Print Universes "dumpfile"Gravatar letouzey2008-11-15
* Faster comparison of universesGravatar letouzey2008-11-14
* retour sur le commit 11579 qui faisait plante les contribs FSet et color.Gravatar soubiran2008-11-14
* Les signatures des applications de foncteur sont précalculées, cela alourdi...Gravatar soubiran2008-11-12
* petite modif du commit 11513.Gravatar soubiran2008-10-28
* Correction bug 1979.Gravatar soubiran2008-10-28
* Correction bug #1969.Gravatar soubiran2008-10-21
* Optimisation de clenv.ml pour que meta_instance ne soit pas appeléGravatar herbelin2008-10-18
* Report des commits 11417 et 11437 de la v8.2Gravatar soubiran2008-10-15
* fixing r11433 again:Gravatar barras2008-10-07
* fixed pb with r11433Gravatar barras2008-10-07
* bug #1951: polymorphic indtypes: universe subst was not performed in the type...Gravatar barras2008-10-06
* added comments in esubst.mliGravatar barras2008-09-09
* Rely on ocamlc to call the C compiler...Gravatar glondu2008-09-04
* fixed minor environment issues when checking inductive typesGravatar barras2008-09-02
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Correction d'une incohérence de typage des inductifs polymorphes: lesGravatar herbelin2008-07-25
* Fixed doc of inductive sort-polymorphism (cf bug #1908). Seized theGravatar herbelin2008-07-23
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* Autour du parsing:Gravatar herbelin2008-07-15
* Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...Gravatar notin2008-06-25
* Les contraintes d'univers sont maintenant collectées dans le champs mod_cons...Gravatar soubiran2008-06-25
* meilleur gestion de la fonction de "cache" des alias (declaremods), et correc...Gravatar soubiran2008-06-18
* correction d'un bug sur la commande Include. Gravatar soubiran2008-06-10
* Ajout d'un comportement special du sous-typage pour les constantes opaques.Gravatar soubiran2008-06-09
* ajout d'un printer pour les contraintes d'univers + correction d'un bug sur l...Gravatar soubiran2008-06-06
* Correction du problème de complexité de Print Assumptions :Gravatar aspiwack2008-05-27
* refined the conversion oracleGravatar barras2008-05-21
* really fixed Georges\' bugGravatar barras2008-05-15
* corrige le bug de GeorgesGravatar barras2008-05-14
* Changement de stratégie vis à vis du commit 10859 sur la gestion desGravatar herbelin2008-05-12
* - Cleanup parsing of binders, reducing to a single production for allGravatar msozeau2008-05-11
* Réutilisation de l'infrastructure pour le polymorphisme d'univers desGravatar herbelin2008-04-30
* Correction du bug des types singletons pas sous-type de SetGravatar herbelin2008-04-27
* correction bug 1839Gravatar soubiran2008-04-25
* Prise en compte des coercions dans les clauses "with" même si le typeGravatar herbelin2008-04-23
* correction d'un bug sur la compostion des substitutions induites par les alia...Gravatar soubiran2008-04-23
* correction du bug sur Parameter Inline que j'ai reouvert hier par inadvertanceGravatar soubiran2008-04-23
* correction bug 1839Gravatar soubiran2008-04-22
* fixed universes bug related to module inclusionGravatar barras2008-04-22
* added the .vo checker (with independent Makefile)Gravatar barras2008-04-21
* - Parameterize unification by two sets of transparent_state, one for openGravatar msozeau2008-04-21
* Correction bug 1838 + doc modules.Gravatar soubiran2008-04-21