index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2003-11-17
Inteprétation des idents filtrés liants dans constrintern.ml (plus robuste)
herbelin
2003-11-17
Un ident filtre est liant seulement si une variable deja liee (sinon bug dans...
herbelin
2003-11-17
maj
filliatr
2003-11-16
Bug filtrage pour inversion notation
herbelin
2003-11-15
Amelioration du message d'erreur en cas de tentative d'instanciation
clrenard
2003-11-15
Bug nommage destruct
herbelin
2003-11-15
Meilleure solution pour la compatibilite
herbelin
2003-11-15
Bug v8 (regles connues etaient re-enregistrees) + tables dans egrammar
herbelin
2003-11-15
Ajout Print Implicit avec depliage du type
herbelin
2003-11-14
MAJ date
herbelin
2003-11-14
Pour les .v8
herbelin
2003-11-14
Move des hyps de NewInduction: retour a situation V7.4 a defaut d'etre robuste
herbelin
2003-11-14
MAJ
herbelin
2003-11-14
Inclusion de Zbool qui contient une partie de Zmisc dans ZArith_base
herbelin
2003-11-14
Conflit renommage
herbelin
2003-11-14
cosmetique
herbelin
2003-11-14
Presentation
herbelin
2003-11-14
Oublis dans les rennomages
herbelin
2003-11-14
Check bavard meme en mode silencieux, car on l'a voulu
herbelin
2003-11-14
Ordre standard pour l'associativite
herbelin
2003-11-14
Quelques oublis pour que les notations marchent bien
herbelin
2003-11-14
Compatibilite %T
herbelin
2003-11-14
Bug implicit arguments
herbelin
2003-11-14
Correction chemin de Z
herbelin
2003-11-14
Automatisation de la traduction de iff_trans; renommage IF
herbelin
2003-11-14
Backtrack sur Peano
herbelin
2003-11-14
Nouveaux lemmes 'canoniques'; compatibilite
herbelin
2003-11-14
Suppression renommages dans Peano
herbelin
2003-11-14
Bug parsing cast
herbelin
2003-11-14
maj
filliatr
2003-11-13
moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc...
barras
2003-11-13
Traduction Print Grammar
herbelin
2003-11-13
Oubli report Nul/Pos
herbelin
2003-11-13
Niveau V8
herbelin
2003-11-13
Fermeture de la section maintenant necessaire
herbelin
2003-11-13
factorisation et generalisation des clauses
barras
2003-11-13
Passage a un SStream predicatif
herbelin
2003-11-13
MAJ
herbelin
2003-11-13
Require
herbelin
2003-11-13
qq petit ajouts à Zdiv
letouzey
2003-11-13
maj
filliatr
2003-11-12
MAJ INZ
herbelin
2003-11-12
MAJ
herbelin
2003-11-12
Bug TacId
herbelin
2003-11-12
Ajout lemme projections
herbelin
2003-11-12
%type au lieu de %T
herbelin
2003-11-12
Lemmes dans un sens plus naturel
herbelin
2003-11-12
Suppression du "..." final !
herbelin
2003-11-12
Restructuration ZArith
herbelin
2003-11-12
Cosmetique
herbelin
[prev]
[next]