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
*
Suppresion de la catégorie des inductifs singletons larges dont
herbelin
2007-02-09
*
Suppression de code mort
notin
2007-02-01
*
suite du commit 9557
soubiran
2007-01-30
*
Petite correction sur un message d'erreur renvoyé au sous typage.
soubiran
2007-01-30
*
modifications des messages d'erreurs renvoyés lors de la comparaison
soubiran
2007-01-24
*
Correction du bug #1315:
notin
2007-01-22
*
Prise en compte des univers algébriques dans les types inférés dans
herbelin
2007-01-19
*
Protection contre les warnings 'unused variable' de ocaml 3.09
herbelin
2007-01-19
*
Correction bug #1302
herbelin
2007-01-17
*
Correction du bug #1273 (problème avec les paramètres non récursivement un...
notin
2006-12-12
*
cosmetique
barras
2006-12-12
*
Changement dans le kernel :
bgregoir
2006-12-11
*
bug condition de garde
barras
2006-12-08
*
Débranchement du polymorphisme de sorte sur les définitions dans Type
herbelin
2006-10-30
*
dependences
barras
2006-10-30
*
Compatibilité du polymorphisme de constantes avec les sections.
herbelin
2006-10-29
*
Extension du polymorphisme de sorte au cas des définitions dans Type.
herbelin
2006-10-28
*
Ajout fold_rel_declaration et fold_named_declaration
herbelin
2006-10-27
*
Correction de 2 bugs critiques du polymorphisme d'univers
herbelin
2006-10-27
*
changement des _sym par _comm dans setoid_ring
bgregoir
2006-10-27
*
Clarification des contraintes sur le contexte de paramètres des
herbelin
2006-10-17
*
Protection raise en début de séquence (en attendant que le code caché trou...
herbelin
2006-10-12
*
Déplacement de on_judgment_type de Typeops vers Termops
herbelin
2006-10-06
*
Correction de deux cas où les types inductifs n'étaient pas comparés
herbelin
2006-10-05
*
Changement de comportement du [rewrite ... in H]: Coq échoue si H
notin
2006-10-03
*
Correction du bug #1181
jforest
2006-09-14
*
Indentation + typo
notin
2006-09-01
*
Ajout iter_rel_context/iter_named_context
herbelin
2006-09-01
*
Appel à caml_modify pour Ocaml 3.07
notin
2006-09-01
*
Export de closedn pour Evarutil
herbelin
2006-08-28
*
correction bug vm_compute
bgregoir
2006-08-25
*
Modifications dans les scripts de configuration (coqtop et coqide affichent m...
notin
2006-07-28
*
- Ajout d'un cast vm dans la syntaxe : x <: t
bgregoir
2006-07-22
*
Correction bug du polymorphisme de sort des inductifs (cas où les variables ...
herbelin
2006-06-22
*
Oh le joli bug dans le kernel:
letouzey
2006-06-05
*
retour au comportement antérieur pour une application de foncteur:
letouzey
2006-05-30
*
- Indtypes: en attente opinion CoRN, les occurrences de Type non explicites
herbelin
2006-05-28
*
Modification de add_glob (support des modules dans Coqdoc)
notin
2006-05-23
*
Ajout substl_named_decl pour mode Maple
herbelin
2006-05-23
*
Nouvelle implantation du polymorphisme de sorte pour les familles inductives
herbelin
2006-05-23
*
Correction trou de typage des éliminations d'inductifs introduit dans commit...
herbelin
2006-05-13
*
correction bugs de condition de garde (fix + cofix)
barras
2006-05-12
*
correction bugs dans Cbv (beta n-aire)
barras
2006-05-10
*
subst. explicites avec vecteurs
barras
2006-05-09
*
amelioration de la machine interpretee (vecteurs au lieu de listes d'arguments)
barras
2006-05-05
*
fixed bug #804: removed useless reduction in fix guard checking
barras
2006-05-03
*
bug #1096: whd_stack on one arg of conversion had side-effect on the other arg
barras
2006-05-03
*
Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...
notin
2006-04-28
*
Standardisation nom option_app en option_map
herbelin
2006-04-27
*
Nouveau mécanisme pour les modules interactifs : les arguments de
herbelin
2006-04-16
[next]