index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
Commit message (
Expand
)
Author
Age
*
simplified proof (eq and eqT are now the same)
barras
2004-06-25
*
Nouveaux thms de non circularité de nat
herbelin
2004-06-02
*
eq2eqT et eqT2eq devenus obsolètes
herbelin
2004-06-02
*
sumbool et sumor affich avec 'if' si possible
herbelin
2004-04-06
*
Commentaires
herbelin
2004-03-29
*
Passage a un 'if-then-else' ou ne sont mentionnes que les membres droits qui ...
herbelin
2004-03-28
*
MAJ commentaires
herbelin
2004-03-24
*
Definition de la notation de la paire par un motif recursif
herbelin
2004-03-17
*
Commentaires
herbelin
2004-03-17
*
ajout decimal_exp pour interpreter les notations decimales
mohring
2004-03-12
*
ide: silent behavior better, save icon, -byte works
marche
2004-03-03
*
MAJ Commentaires
herbelin
2004-02-28
*
Ajout delimiteur pour bool_scope
herbelin
2004-02-12
*
Décomposition automatique des règles d'analyse syntaxique pour les
herbelin
2004-02-12
*
backtrack implicit dans Bvector
marche
2004-02-10
*
patch Bvector: args implicites
marche
2004-02-09
*
MAJ simplification
herbelin
2004-01-27
*
Suppression de Rsyntax en v8
herbelin
2004-01-13
*
bugs avec Pose et Assert
barras
2004-01-09
*
Commentaires en v8
herbelin
2004-01-09
*
Ajout delimiteur et arguments de scope pour list
herbelin
2003-12-24
*
changement de pose en set (pose n'etait pas utilise avec la semantique
barras
2003-12-24
*
Finalement, espacement autour du ':' pour a la fois exists, forall et fun
herbelin
2003-12-23
*
Affichage sur le modèle du forall pour le exists
herbelin
2003-12-21
*
Duplication temporaire des règles de syntaxe des paires
herbelin
2003-12-16
*
modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixes
barras
2003-12-15
*
power associe a droite
marche
2003-12-05
*
Suppression du niveau 250 vide car pose des problemes avec camlp4; remplace p...
herbelin
2003-12-04
*
Ratage standardisation Rge_monotony en Rmult_ge_compat_r
herbelin
2003-12-01
*
Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...
herbelin
2003-11-29
*
Notation locale pour Rpower
herbelin
2003-11-29
*
Ajout lemmes, simplification preuve de SeqProp
herbelin
2003-11-29
*
ground->firstorder, cc-> congruence, CC final commit
corbinea
2003-11-29
*
Utilisation du total_order non constructif
herbelin
2003-11-29
*
Report de lemmes de Znumtheory dans Zabs ou BinInt
herbelin
2003-11-29
*
Protection contre les renommages; redondances
herbelin
2003-11-28
*
Renoncement de la compatibilite des noms qualifies au profit de la compatibil...
herbelin
2003-11-24
*
Compatibilite
herbelin
2003-11-22
*
Simplification; ajout Zcompare_antisym
herbelin
2003-11-21
*
ajout Pnat (suite)
herbelin
2003-11-21
*
ajout Pnat (suite)
herbelin
2003-11-21
*
Extraction des lemmes sur convert/nat_of_P de BinPos vers Pnat; ajout Pcase e...
herbelin
2003-11-21
*
Tri et typo
herbelin
2003-11-21
*
ajout de Znumtheory.v dans ZArith
letouzey
2003-11-19
*
Restauration compatibilite 7.4 pour le Hint Unfold Rgt
herbelin
2003-11-19
*
Un nouveau lemme redondant ...
herbelin
2003-11-18
*
Deplacement ZERO_le_inj dans Zorder
herbelin
2003-11-18
*
Meilleure solution pour la compatibilite
herbelin
2003-11-15
*
Pour les .v8
herbelin
2003-11-14
*
Inclusion de Zbool qui contient une partie de Zmisc dans ZArith_base
herbelin
2003-11-14
[next]