index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
theories
/
Reals
/
Rbase.v
Age
Commit message (
Expand
)
Author
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2018-02-27
Update headers following #6543.
Théo Zimmermann
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2016-01-20
Update copyright headers.
Maxime Dénès
2015-01-12
Update headers.
Maxime Dénès
2012-08-08
Updating headers.
herbelin
2010-07-24
Updated all headers for 8.3 and trunk
herbelin
2010-04-29
Remove the svn-specific $Id$ annotations
letouzey
2006-09-26
mise a jour du nouveau ring et ajout du nouveau field, avant renommages
barras
2004-07-16
Nouvelle en-tête
herbelin
2003-11-29
Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...
herbelin
2003-09-23
Fusion des fichiers de syntaxe de Init avec les fichiers de définition; Type...
herbelin
2003-01-16
Renommage de RealsB en Rbase
desmettr
2003-01-15
Nouvelle interprétation des nombres réels
desmettr
2002-11-27
Réorganisation de la librairie des réels
desmettr
2002-06-20
*** empty log message ***
desmettr
2002-05-31
Ajout d'occurrences de Field (ne pas enlever)
delahaye
2002-05-29
Double Induction prend maintenant des noms d'hyppthèses
herbelin
2002-04-17
Uniformisation (Qed/Save et Implicits Arguments)
herbelin
2002-04-02
Optimisation
desmettr
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-02-14
option -dump-glob pour coqdoc
filliatr
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-11-30
Integration de nouveaux lemmes
desmettr
2001-11-30
*** empty log message ***
desmettr
2001-11-30
Intégration de nouveaux lemmes.
desmettr
2001-08-05
Expérimentation de NewDestruct et parfois NewInduction
herbelin
2001-06-19
Oubli Save + je sais plus
mayero
2001-06-18
Ajouts de lemmes (pour Float)
mayero
2001-04-23
Ajouts Reals
mayero
2001-04-23
Minor layout adjustments for Library doc
coq
2001-04-20
Ajout tactics Reals
mayero
2001-04-20
Library doc adjustments (until page 140)
coq
2001-04-19
Changement syntax pour Rinv
mayero
2001-04-19
Ajout de Field
delahaye
2001-03-15
entetes
filliatr
2001-02-14
Renommage des variables dans les schémas d'induction
herbelin
2001-01-25
Modif de l'axiomatisation pour enlever les /\ de _ne
mayero
2001-01-11
Mise a jour Rbase
mohring
2000-11-23
Ajout d'une syntaxe pour Reals.
mayero
2000-11-10
mise-a-jour, ajouts de quelques truc...
mayero
2000-11-05
Pour ne plus éviter temporairement le "Auto with zarith" !
herbelin
2000-10-30
Pour eviter temporairement le "Auto with zarith"
delahaye
2000-06-21
theories/Reals
filliatr