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
*
NEW*VO doit apparaitre apres *VO + divers
herbelin
2003-10-04
*
maj
filliatr
2003-10-04
*
pr_vernac est paresseux; States.unfreeze seulement après que msgnl ait
herbelin
2003-10-03
*
Bug cible newtheories/Init + divers
herbelin
2003-10-03
*
Cacher les .v8
herbelin
2003-10-03
*
Correction bug explosion de la taille de la liste loaded_modules
herbelin
2003-10-03
*
Nettoyage, simplification et compatibilite -j
herbelin
2003-10-03
*
oubli de deux flags -v7
letouzey
2003-10-03
*
*** empty log message ***
barras
2003-10-03
*
Pas de renommage des noms de section
herbelin
2003-10-02
*
as au niveau de app
herbelin
2003-10-02
*
Hypothesis mot-cle
herbelin
2003-10-02
*
Traduction des tests success et test en v8
herbelin
2003-10-02
*
Plus de nom commencant par '_' en V8
herbelin
2003-10-02
*
Le nom '_' n'est plus valable en v8 pour nommer les variables
herbelin
2003-10-02
*
Retour sur la version non optimisee de 'add' pour compatibilite; renommage Un...
herbelin
2003-10-01
*
cosmetique
herbelin
2003-10-01
*
Implantation de l'option 'format' des Notations
herbelin
2003-10-01
*
maj
filliatr
2003-10-01
*
'_ = _ = _' maintenant predefini, meme en V7
herbelin
2003-09-30
*
Ajout 'Close Scope', mise en place de la structure pour un modificateur 'format'
herbelin
2003-09-30
*
Les notations hors scope s'empilent maintenant comme des scopes ne
herbelin
2003-09-30
*
code mort
herbelin
2003-09-30
*
Les notations hors scope s'empilent maintenant comme des scopes ne
herbelin
2003-09-30
*
Ajout 'Close Scope'.
herbelin
2003-09-30
*
Ajout 'Close Scope'.
herbelin
2003-09-30
*
Ajout 'Close Scope'.
herbelin
2003-09-30
*
Oubli du type du terme a filtrer quand pas d'argument dans la traduction de case
herbelin
2003-09-29
*
Prise en compte d'un inductif sans argument dans le 'in' des 'match'
herbelin
2003-09-29
*
oups
letouzey
2003-09-28
*
2 pbs de plus réglés concernant Setoid Ring:
letouzey
2003-09-28
*
une induction de moins dans lt_eq_lt_dec
letouzey
2003-09-28
*
well_founded_induction de nouveau transparent
letouzey
2003-09-28
*
maj
filliatr
2003-09-27
*
Bug about
herbelin
2003-09-26
*
Syntaxe plus liberale pour le type des arguments de filtrage du 'match'
herbelin
2003-09-26
*
Syntaxe plus liberale pour le type des arguments de filtrage du 'match'; trad...
herbelin
2003-09-26
*
MAJ
herbelin
2003-09-26
*
pa_ifdef.cmo redondant
herbelin
2003-09-26
*
Ajout now_show
herbelin
2003-09-26
*
About, Infix
herbelin
2003-09-26
*
'Open Local Scope' en attendant que le core_scope sache se mettre devant impl...
herbelin
2003-09-26
*
Ajout 'About'
herbelin
2003-09-26
*
Induction -> NewInduction; '++' pour app
herbelin
2003-09-26
*
Nouvelle serie de traductions
herbelin
2003-09-26
*
Re-possibilite changement chaine infixe en passant v7 a v8
herbelin
2003-09-26
*
Passage de Destruct a NewDestruct; '-' pour negb
herbelin
2003-09-26
*
Structuration de fast_integer en operations sur positive, proprietes des oper...
herbelin
2003-09-26
*
Un peu plus de souplesse dans la globalisation des noms utilises par les tact...
herbelin
2003-09-26
*
Decouplage printing en v8 pour les interpretations de notations
herbelin
2003-09-26
[next]