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
*
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
*
Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ...
herbelin
2003-10-30
*
Choix sous sa forme relationnelle
herbelin
2003-10-29
*
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 %core; MAJ niveau connecteurs logique
herbelin
2003-10-28
*
MAJ
herbelin
2003-10-28
*
Fichier offrant l'axiome du choix unique en presence de logique classique
herbelin
2003-10-28
*
Fichier offrant l'axiome du choix en presence de logique classique
herbelin
2003-10-28
*
La logique sur Type inclut celle sur Set
herbelin
2003-10-28
*
Retour en arriere sur d'autres renommages de variables
herbelin
2003-10-28
*
Retour a un nommage non standard des variables pour compatibilite; report 're...
herbelin
2003-10-27
*
Bug du commit precedent
herbelin
2003-10-27
*
Commentaires
herbelin
2003-10-23
*
Documentation/Structuration
herbelin
2003-10-22
*
Documentation/Structuration
herbelin
2003-10-22
*
reorganisation des niveaux (ex: = est a 70)
barras
2003-10-22
*
Redondance de dec_eq_nat
herbelin
2003-10-21
*
Type relation dans Datatypes
herbelin
2003-10-21
*
Maintenant avant Datatypes
herbelin
2003-10-21
*
ajouts
herbelin
2003-10-21
*
R passe dans Set !
herbelin
2003-10-20
*
20 est uniquement associatif a gauche
herbelin
2003-10-17
*
Des implicites plus 'naturels' pour eq_ind, identity_ind and co
herbelin
2003-10-17
*
nouvelle syntaxe de ltac
barras
2003-10-16
*
lettac -> set
barras
2003-10-16
*
Syntax error
herbelin
2003-10-16
*
Suppression des surcharge de regles de grammaire en v7
herbelin
2003-10-16
*
Pour eviter des regles redondantes en v7
herbelin
2003-10-16
*
FTC_P2 maintenant dans RIneq
herbelin
2003-10-16
*
Ajout de quelques lemmes cles
herbelin
2003-10-16
*
Affichage = au lieu de == en v7
herbelin
2003-10-15
*
Nettoyage argument de nil
herbelin
2003-10-15
*
Changement 'as notation' en 'where notation'
herbelin
2003-10-14
*
Argument de except, error implicite seulement en v8; Changement 'as notation'...
herbelin
2003-10-14
*
Argument de None implicite seulement en v8
herbelin
2003-10-14
*
Argument implicite pour None, error, except
herbelin
2003-10-13
*
Notations pour l'exponentiation
herbelin
2003-10-13
*
Enregistrement '^' en v8
herbelin
2003-10-13
*
mise a jour nouvelle syntaxe
barras
2003-10-11
*
nat_scope ouvert par defaut
herbelin
2003-10-10
*
identity est equivalent sur Type (sauf sans argument)
herbelin
2003-10-10
*
type_scope
herbelin
2003-10-10
*
Suppression de definitions equivalentes
herbelin
2003-10-10
*
Notation '^'
herbelin
2003-10-10
*
Plus d'Eval Compute
herbelin
2003-10-10
*
MAJ commentaires
herbelin
2003-10-10
*
Delimiters N devient 'nat'
herbelin
2003-10-10
[next]