index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
Deplacement de le_minus de fast_integer vers Minus
herbelin
2003-06-14
*
Deplacement de le_minus de fast_integer vers Minus
herbelin
2003-06-14
*
maj
filliatr
2003-06-14
*
changement de spécif du fold
letouzey
2003-06-13
*
Ground update
corbinea
2003-06-13
*
CoqIDE: undo plus efficace sur les inductifs
filliatr
2003-06-13
*
Ground update, new files.
corbinea
2003-06-13
*
coqide: indentation
monate
2003-06-13
*
Utilisation de intro_pattern dans NewDestruct/NewInduction
herbelin
2003-06-13
*
fcts tail-recursives
filliatr
2003-06-13
*
Require Export
filliatr
2003-06-13
*
install-fsets
filliatr
2003-06-13
*
FSets, mais pas compile' par make world
filliatr
2003-06-13
*
suite changements ZArith en vu de librairie FSet
letouzey
2003-06-13
*
quelques adaptations de Zarith en vu de la nouvelle librarie FSet
letouzey
2003-06-13
*
coqide: about now displays versions/Fix for alt-enter
monate
2003-06-13
*
Deplacement d'un lemme sur nat de ZArith vers Arith
herbelin
2003-06-13
*
CoqIDE: undo immediat sur les commandes ne modifiant pas l'etat
filliatr
2003-06-13
*
Ground update.
corbinea
2003-06-13
*
enieme correction du nommage modulaire
letouzey
2003-06-12
*
fin de l'affichage des signatures de modules dans les *.ml
letouzey
2003-06-12
*
MAJ
herbelin
2003-06-12
*
INZ reste constante pour compat V7 mais Unfold INZ est supprimé par le tradu...
herbelin
2003-06-12
*
Ajout option translate_syntax pour caractériser l'interprétation du traduct...
herbelin
2003-06-12
*
Pb quand une meme classe est definie dans 2 fichiers
herbelin
2003-06-11
*
Token '.(' seulement pour v8, sinon conflit avec '.(*'
herbelin
2003-06-11
*
maj
filliatr
2003-06-11
*
MAJ
herbelin
2003-06-10
*
Typo
herbelin
2003-06-10
*
Module Bij inutilise
herbelin
2003-06-10
*
Import nat_scope
herbelin
2003-06-10
*
Suppression d'une occurrence superflue d'argument de type dans Notation sacha...
herbelin
2003-06-10
*
Deplacement delimiteur T dans Notations
herbelin
2003-06-10
*
Module Bij inutilise
herbelin
2003-06-10
*
Ajout notation c.(f) en v8 pour les projections de Record
herbelin
2003-06-10
*
freshid -> fresh
herbelin
2003-06-10
*
Déplacement traducteur de nom dans Constrextern pour accès aux noms longs
herbelin
2003-06-10
*
Réinstallation d'un afficheur de niveau d'imbrication pour le déboggueur de...
herbelin
2003-06-10
*
Simplification case_info
herbelin
2003-06-10
*
Ajout notation c.(f) en v8 pour les projections de Record; raffinement divers
herbelin
2003-06-10
*
Raffinement divers
herbelin
2003-06-10
*
Globalisation des tactiques avant traduction pour capture des noms; affinemen...
herbelin
2003-06-10
*
Distinction mode v7 ou translate; conséquences du déplacement traducteur de...
herbelin
2003-06-10
*
Déplacement de code dans command; MAJ DebugOn
herbelin
2003-06-10
*
Mise en place structure pour des 'arguments scope' dirigés par une classe
herbelin
2003-06-10
*
Amélioration afficheur de Cases pour les constr_pattern
herbelin
2003-06-10
*
Passage des noms de tactiques à kernel_name pour compatibilité avec les fon...
herbelin
2003-06-10
*
Déplacement traducteur de nom dans Constrextern pour accès aux noms longs
herbelin
2003-06-10
*
Ajout notation c.(f) en v8 pour les projections de Record
herbelin
2003-06-10
*
Factorisation de detype_case pour utilisation par l'afficheur de pattern
herbelin
2003-06-10
[next]