index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
theories
/
Reals
Age
Commit message (
Expand
)
Author
2002-04-17
Uniformisation (Qed/Save et Implicits Arguments)
herbelin
2002-04-02
Optimisation
desmettr
2002-04-02
Suppression PI_lb et PI_ub
desmettr
2002-04-02
Suppression Field
desmettr
2002-03-29
sans utiliser Field
desmettr
2002-03-29
Suppression des invocations a Field
desmettr
2002-03-22
Bug d'affichage des réels dû à une collision entre les APPLINSIDETAIL de Z...
herbelin
2002-03-21
Intuition ne fait plus de Unfold des constantes (il faut les faire
courant
2002-03-20
Intuition now takes an (optional) tactic as parameter. This tactic is
courant
2002-03-19
Exportation de SplitRmult et SplitAbsolu
delahaye
2002-03-17
Field ne fait maintenant que les reductions necessaires
delahaye
2002-03-07
*** empty log message ***
desmettr
2002-02-14
option -dump-glob pour coqdoc
filliatr
2002-01-07
Ajout en-tête
herbelin
2001-12-21
Passage coqweb
herbelin
2001-12-19
*** empty log message ***
desmettr
2001-12-07
*** empty log message ***
desmettr
2001-12-07
*** 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
*** empty log message ***
desmettr
2001-12-04
Traitement t de -1<>0
delahaye
2001-12-04
Backtrack sur le commit du 30.11.2001
delahaye
2001-12-03
*** empty log message ***
desmettr
2001-11-30
*** 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-10-23
Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrR
delahaye
2001-09-18
modif test const
mayero
2001-09-11
Un look un peu plus avenant aux productions des règles de grammaire
herbelin
2001-08-05
Expérimentation de NewDestruct et parfois NewInduction
herbelin
2001-07-19
modifs de preuves (plus simples)
mayero
2001-06-19
Oubli Save + je sais plus
mayero
2001-06-18
Ajouts de lemmes (pour Float)
mayero
2001-06-04
Correction bug outside
mayero
2001-05-07
ex d'utilisation de fourier avec field
mayero
2001-04-25
coqweb
filliatr
2001-04-24
correction nom
mayero
2001-04-24
Ajout de Rseries et Rtrigo_fun
mayero
2001-04-24
(Again) Little corrections for Library doc
coq
[next]