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
*
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
*
Ajout du paradoxe de Berardi dans Logic (preuve que EM => PI dans CCI)
barras
2001-06-18
*
Correction bug outside
mayero
2001-06-04
*
Creation du fichier Zhints.v repertoriant les thms de ZArith et definissant l...
herbelin
2001-05-31
*
Correction d'un bug du pretty-print
clrenard
2001-05-29
*
Modification pour passage p-automates
mohring
2001-05-15
*
ex d'utilisation de fourier avec field
mayero
2001-05-07
*
coqweb
filliatr
2001-04-25
*
correction nom
mayero
2001-04-24
*
Ajout de Rseries et Rtrigo_fun
mayero
2001-04-24
*
(Again) Little corrections for Library doc
coq
2001-04-24
*
Ajout Reals
mayero
2001-04-23
*
Ajouts Reals
mayero
2001-04-23
*
(One more) Minor layout adjustments for Library doc
coq
2001-04-23
*
Minor layout adjustments for Library doc
coq
2001-04-23
*
Ajout tactics Reals
mayero
2001-04-20
*
Library doc adjustments (until page 140)
coq
2001-04-20
*
typo
filliatr
2001-04-19
*
Ajout de fonctions proposees par Cuiht Alvarado
mohring
2001-04-19
*
BoolEq.v, une egalite generique a valeur dans bool
mohring
2001-04-19
*
remplace Zarith par ZArith
mohring
2001-04-19
*
remplace Zarith par ZArith
mohring
2001-04-19
*
Mise de (*i autour CVS info
mohring
2001-04-19
*
Mise de (*i autour CVS info
mohring
2001-04-19
*
Mise de (*i autour CVS info
mohring
2001-04-19
*
*** empty log message ***
mohring
2001-04-19
*
Remplacement Euclid_def Euclid_proof par Euclid
mohring
2001-04-19
*
Changement syntax pour Rinv
mayero
2001-04-19
[next]