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
...
*
Rien de bien important
herbelin
2003-11-02
*
Commentaires
herbelin
2003-11-02
*
MAJ
herbelin
2003-11-02
*
Le printeur de Show Script n'etait pas le bon en v7
herbelin
2003-11-02
*
Typo
herbelin
2003-11-02
*
Ajout Diaconescu.v
herbelin
2003-11-02
*
AC + EXT -> EM
herbelin
2003-11-02
*
Relations entre le choix (forme relationnelle) avec restriction ou non
herbelin
2003-11-02
*
Renommage bool en boolP pour eviter la qualification
herbelin
2003-11-02
*
Restauration preference Rge a Rle pour compatibilite...
herbelin
2003-11-02
*
Restauration preference Rge a Rle pour compatibilite...; petit nettoyage
herbelin
2003-11-02
*
Protection contre les buts sans inegalite
herbelin
2003-11-02
*
Ajout CPatNotation, PrintVisibility
herbelin
2003-11-01
*
Extensibilite de la grammaires des patterns
herbelin
2003-11-01
*
Renommage Topconstr.map_aconstr_with_binders_loc
herbelin
2003-11-01
*
Fusion de l'univers et du nom d'entree en un 'Print Grammar entry' en v8
herbelin
2003-11-01
*
Il ne faut pas mettre le constrarg des tactiques au niveau lconstr
herbelin
2003-11-01
*
Extensibilite de la grammaires des patterns
herbelin
2003-11-01
*
Traduction des noms pour les refs de pr_glob_generic (via pr_global)
herbelin
2003-11-01
*
Utilisation de niveaux pour l'extensibilite de la grammaires des patterns
herbelin
2003-11-01
*
Extension de get_constr_entry et symbol_of_production pour gerer les extensio...
herbelin
2003-11-01
*
Pas de defaut a 1 et LeftA pour les infixes v8; fusion de l'univers et du nom...
herbelin
2003-11-01
*
Ajout notations pour motifs de Cases; renommage map_aconstr_with_binders_loc
herbelin
2003-11-01
*
Ajout CPatNotation; renommage map_aconstr_with_binders_loc
herbelin
2003-11-01
*
Finalement, niveau 0 pour l'argument du '-' unaire, pour éviter que
herbelin
2003-11-01
*
Controle par le prefixe et plus par le nom absolu pour la recherche d'objets ...
herbelin
2003-11-01
*
Interdiction de nommer un object de nom commencant par Coq en dehors de la bi...
herbelin
2003-11-01
*
Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie...
herbelin
2003-11-01
*
Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie...
herbelin
2003-11-01
*
Heritage des notations v7 seulement si zero information v8
herbelin
2003-11-01
*
Debranchement de Print si pas verbose (necessaire pour traducteur)
herbelin
2003-11-01
*
maj
filliatr
2003-10-31
*
Redirected some of the verbose jprover output through the Pp module.
corbinea
2003-10-30
*
Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ...
herbelin
2003-10-30
*
Affichage des negatifs au niveau de l'application, et des positifs au dessus ...
herbelin
2003-10-30
*
traduction des noms de correctness
herbelin
2003-10-30
*
*** empty log message ***
herbelin
2003-10-29
*
Choix sous sa forme relationnelle
herbelin
2003-10-29
*
maj
filliatr
2003-10-29
*
MAJ
herbelin
2003-10-28
*
Ordre (symbolique) des Require
herbelin
2003-10-28
*
Passage de la notations de paire dans core_scope
herbelin
2003-10-28
*
Passage des notations de type dans type_scope
herbelin
2003-10-28
*
Ajout notations pour les expressions dans un anneau
herbelin
2003-10-28
*
Simplification preuve
herbelin
2003-10-28
*
Ajout de Print Visibility
herbelin
2003-10-28
*
Ajout %core; MAJ niveau connecteurs logique
herbelin
2003-10-28
*
Affichage Assert_failure en ocaml 3.07
herbelin
2003-10-28
*
Message inductive large
herbelin
2003-10-28
*
Nouveaux fichiers dans Logic
herbelin
2003-10-28
[prev]
[next]