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
*
*** empty log message ***
desmettr
2001-12-07
*
*** empty log message ***
desmettr
2001-12-07
*
Amélioration nommage hypothèses NewInduction (et incompatibilités)
herbelin
2001-12-06
*
*** empty log message ***
desmettr
2001-12-05
*
*** empty log message ***
desmettr
2001-12-05
*
*** empty log message ***
desmettr
2001-12-05
*
*** empty log message ***
desmettr
2001-12-05
*
*** empty log message ***
desmettr
2001-12-05
*
*** empty log message ***
desmettr
2001-12-05
*
*** empty log message ***
desmettr
2001-12-05
*
Traitement t de -1<>0
delahaye
2001-12-04
*
Backtrack sur le commit du 30.11.2001
delahaye
2001-12-04
*
*** empty log message ***
desmettr
2001-12-03
*
*** empty log message ***
desmettr
2001-11-30
*
*** empty log message ***
desmettr
2001-11-30
*
*** empty log message ***
desmettr
2001-11-30
*
Ajout du fichier
desmettr
2001-11-30
*
Modification de Reals pour integrer les modifications
desmettr
2001-11-30
*
Ajout du fichier concernant le carre et la racine carree
desmettr
2001-11-30
*
Integration de nouveaux lemmes
desmettr
2001-11-30
*
*** empty log message ***
desmettr
2001-11-30
*
Intégration de nouveaux lemmes.
desmettr
2001-11-30
*
remise au gout du jour du repertoire theories/Sorting de la V6.3
letouzey
2001-11-21
*
Ajout d'un fichier Max dans Arith, et enrichissement du Min.
letouzey
2001-11-15
*
Ajout des fonctions tail-recursives tail_plus et tail_mult.
letouzey
2001-11-15
*
Suppression d'Export redondants
herbelin
2001-11-14
*
suppression d'axiomes dans Rstar, Newman et Integers
letouzey
2001-11-12
*
interversion de deux Elim dans In_dec pour que la fonction extraite soit effi...
letouzey
2001-11-03
*
Suppression de Logic_Type.sigT, redondant avec Specif.sigT
herbelin
2001-10-24
*
Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrR
delahaye
2001-10-23
*
Simplification de deux preuves. En outre ca simplifie leur extraction.
letouzey
2001-09-27
*
and_rec redondant
letouzey
2001-09-27
*
Transparent
barras
2001-09-20
*
Deplacement des setoides.
clrenard
2001-09-19
*
Modification de l'emplacement des fichiers pour les setoides.
clrenard
2001-09-18
*
modif test const
mayero
2001-09-18
*
Rustine pour gérer inject_nat
herbelin
2001-09-12
*
Un look un peu plus avenant aux productions des règles de grammaire
herbelin
2001-09-11
*
Du bon usage des commentaires coqweb
herbelin
2001-09-11
*
Conformité des commentaires au format coqweb
herbelin
2001-09-11
*
Fin de la modif Exc/option
mohring
2001-08-30
*
ajout option , Exc --> option, et lemmes dans les theories
mohring
2001-08-29
*
Rétablissement nom de section Map après résolution bugs surcharge de noms
herbelin
2001-08-13
*
Protection des commentaires pour coqtex et coqweb
herbelin
2001-08-13
*
Expérimentation de NewDestruct et parfois NewInduction
herbelin
2001-08-05
*
modifs de preuves (plus simples)
mayero
2001-07-19
*
modif Map section
mohring
2001-07-16
*
Ajout du .v pour la tactique Setoid_replace
clrenard
2001-07-10
*
Oubli Save + je sais plus
mayero
2001-06-19
*
Ajouts de lemmes (pour Float)
mayero
2001-06-18
[next]