index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
Commit message (
Expand
)
Author
Age
*
petite modif du commit 11513.
soubiran
2008-10-28
*
Correction bug 1979.
soubiran
2008-10-28
*
Correction bug #1969.
soubiran
2008-10-21
*
Optimisation de clenv.ml pour que meta_instance ne soit pas appelé
herbelin
2008-10-18
*
Report des commits 11417 et 11437 de la v8.2
soubiran
2008-10-15
*
fixing r11433 again:
barras
2008-10-07
*
fixed pb with r11433
barras
2008-10-07
*
bug #1951: polymorphic indtypes: universe subst was not performed in the type...
barras
2008-10-06
*
added comments in esubst.mli
barras
2008-09-09
*
Rely on ocamlc to call the C compiler...
glondu
2008-09-04
*
fixed minor environment issues when checking inductive types
barras
2008-09-02
*
Évolutions diverses et variées.
herbelin
2008-08-04
*
Correction d'une incohérence de typage des inductifs polymorphes: les
herbelin
2008-07-25
*
Fixed doc of inductive sort-polymorphism (cf bug #1908). Seized the
herbelin
2008-07-23
*
Uniformisation du format des messages d'erreur (commencent par une
herbelin
2008-07-17
*
Autour du parsing:
herbelin
2008-07-15
*
Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...
notin
2008-06-25
*
Les contraintes d'univers sont maintenant collectées dans le champs mod_cons...
soubiran
2008-06-25
*
meilleur gestion de la fonction de "cache" des alias (declaremods), et correc...
soubiran
2008-06-18
*
correction d'un bug sur la commande Include.
soubiran
2008-06-10
*
Ajout d'un comportement special du sous-typage pour les constantes opaques.
soubiran
2008-06-09
*
ajout d'un printer pour les contraintes d'univers + correction d'un bug sur l...
soubiran
2008-06-06
*
Correction du problème de complexité de Print Assumptions :
aspiwack
2008-05-27
*
refined the conversion oracle
barras
2008-05-21
*
really fixed Georges\' bug
barras
2008-05-15
*
corrige le bug de Georges
barras
2008-05-14
*
Changement de stratégie vis à vis du commit 10859 sur la gestion des
herbelin
2008-05-12
*
- Cleanup parsing of binders, reducing to a single production for all
msozeau
2008-05-11
*
Réutilisation de l'infrastructure pour le polymorphisme d'univers des
herbelin
2008-04-30
*
Correction du bug des types singletons pas sous-type de Set
herbelin
2008-04-27
*
correction bug 1839
soubiran
2008-04-25
*
Prise en compte des coercions dans les clauses "with" même si le type
herbelin
2008-04-23
*
correction d'un bug sur la compostion des substitutions induites par les alia...
soubiran
2008-04-23
*
correction du bug sur Parameter Inline que j'ai reouvert hier par inadvertance
soubiran
2008-04-23
*
correction bug 1839
soubiran
2008-04-22
*
fixed universes bug related to module inclusion
barras
2008-04-22
*
added the .vo checker (with independent Makefile)
barras
2008-04-21
*
- Parameterize unification by two sets of transparent_state, one for open
msozeau
2008-04-21
*
Correction bug 1838 + doc modules.
soubiran
2008-04-21
*
Add the ability to give a transparent_state for conversion, to
msozeau
2008-04-20
*
suite 10790 (identificateurs)
herbelin
2008-04-14
*
Bugs, nettoyage, et améliorations diverses
herbelin
2008-04-13
*
Patch sur le typage d'un foncteur applique a un alias.
soubiran
2008-04-03
*
Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient
herbelin
2008-04-01
*
- Second pass on implementation of let pattern. Parse "let ' par [as x]?
msozeau
2008-03-28
*
Correction d'un bug sur Import/Export : ces fonctionnalites sont gerees en-de...
soubiran
2008-03-26
*
Correction de bugs relatifs a la compostion des substitutions
soubiran
2008-03-25
*
improved the implementation of rtree
barras
2008-03-18
*
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10690 85f007b7-540e-0...
barras
2008-03-18
*
Application de refresh_universes dans typing.ml et retyping.ml : les
herbelin
2008-03-15
[next]