index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
/
Logic
Commit message (
Expand
)
Author
Age
*
Passage de Set à Type dans Relations et Wellfounded
herbelin
2007-02-06
*
Correction typo eq_rec_eq (cf bug #1339)
herbelin
2007-01-31
*
Derivation of (exists x : A, P x) -> {x : A | P x} for decidable P
emakarov
2007-01-23
*
Clarification redondance Axiome du choix unique/description
herbelin
2007-01-22
*
Remplacement axiome JMeq_eq dans BinPos par eq_dec_eq sur type à
herbelin
2006-12-28
*
AllÃègement de syntxe suite à l'introduction de l'unif pattern
herbelin
2006-12-12
*
Mise en forme des theories
notin
2006-10-17
*
Passage à une définition de inhabited plus dans les 'standard mathématique...
herbelin
2006-08-28
*
"Essai de remplacement de "ex P" par "exists x, P x" suite à
herbelin
2006-08-28
*
JMeq maintenant applicable sur Type
herbelin
2006-08-24
*
Typo
herbelin
2006-07-06
*
MAJ du manuel de référence
notin
2006-07-04
*
Déplacement Int.v dans ZArith, déplacement de DecidableType.v et DecidableT...
herbelin
2006-06-09
*
Ajout exists! et restructuration/extension des fichiers sur la
herbelin
2006-06-04
*
Ajout exists! et restructuration/extension des fichiers sur la
herbelin
2006-06-04
*
Standardisation du nom des méthodes de Evd
herbelin
2006-04-28
*
Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...
notin
2006-04-28
*
Réajout de eq_rec_eq oublié lors de la modularisation de Eqdep
herbelin
2006-03-30
*
Modification des propriétés (svn:executable)
notin
2006-03-17
*
Modularisation des preuves concernant la logique classique, l'indiscernabilit...
herbelin
2006-03-05
*
Commentaires
herbelin
2006-03-05
*
Renommage du IP classique pour éviter confusion avec IP constructif
herbelin
2006-03-05
*
Ajout étude IP généralisé, Gödel-Dummett, buveur
herbelin
2006-03-05
*
Petite simplification en passant
herbelin
2006-03-04
*
add a left and right tactic for classical logic
narboux
2005-07-15
*
MAJ changements ChoiceFacts
herbelin
2004-12-05
*
Paramétrisation du domaine des axiomes de choix + ajout description = choice...
herbelin
2004-12-05
*
MAJ commentaire sur incohérence EM dans Set
herbelin
2004-11-07
*
Réponse à la conjecture que PI est indépendant de EM dans CC
herbelin
2004-11-02
*
Minimisation utilisation NNPP
herbelin
2004-08-03
*
Déclaration d'obsolescence
herbelin
2004-08-03
*
Typo
herbelin
2004-08-03
*
Ref
herbelin
2004-08-03
*
Commentaires coqdoc
herbelin
2004-08-01
*
Commentaires coqdoc
herbelin
2004-08-01
*
Nouvelle en-tête
herbelin
2004-07-16
*
simplified proof (eq and eqT are now the same)
barras
2004-06-25
*
eq2eqT et eqT2eq devenus obsolètes
herbelin
2004-06-02
*
MAJ commentaires
herbelin
2004-03-24
*
Commentaires
herbelin
2004-03-17
*
MAJ simplification
herbelin
2004-01-27
*
changement de pose en set (pose n'etait pas utilise avec la semantique
barras
2003-12-24
*
modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixes
barras
2003-12-15
*
Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...
herbelin
2003-11-29
*
Biblio standard sans mention de la possibilite d'etre impredicatif
herbelin
2003-11-07
*
Biblio standard sans impredicativite
herbelin
2003-11-07
*
Preuve de l'incoherence de {A}+{~A} avec Set impredicatif
herbelin
2003-11-05
*
Cosmetique
herbelin
2003-11-02
*
Renforcement significatif du resultat principal
herbelin
2003-11-02
*
Rien de bien important
herbelin
2003-11-02
[next]