index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
/
Reals
/
Rfunctions.v
Commit message (
Expand
)
Author
Age
*
Open Local Scope ---> Local Open Scope, same with Notation and alii
letouzey
2012-07-05
*
ZArith + other : favor the use of modern names instead of compat notations
letouzey
2012-07-05
*
Modifications and rearrangements to remove the action that sin (PI/2) = 1
bertot
2012-06-05
*
BinInt: Z.add become the alternative Z.add'
letouzey
2011-05-05
*
Remove the "Boxed" syntaxes and the const_entry_boxed field
letouzey
2011-01-28
*
Some more revision of {P,N,Z}Arith + bitwise ops in Ndigits
letouzey
2010-11-18
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Remove various useless {struct} annotations
letouzey
2009-11-02
*
Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'
letouzey
2009-10-08
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Added the following lemmas to homogenize Reals a bit:
gmelquio
2009-09-11
*
Renoncement à rationaliser les Hints "real" vis à vis de Rle/Rge et Rlt/Rgt :
herbelin
2008-04-06
*
Suite 10760
herbelin
2008-04-05
*
Une passe sur les réels:
herbelin
2008-03-23
*
Changement dans ring et field, beaucoup de correction d'erreurs,
bgregoir
2006-12-15
*
Changement dans le kernel :
bgregoir
2006-12-11
*
simplif de la partie ML de ring/field
barras
2006-10-27
*
Mise en forme des theories
notin
2006-10-17
*
commit de field + renommages
barras
2006-09-26
*
mise a jour du nouveau ring et ajout du nouveau field, avant renommages
barras
2006-09-26
*
compatibility with POWERPC
gregoire
2004-11-22
*
Changement dans les boxed values .
gregoire
2004-11-12
*
COMMITED BYTECODE COMPILER
barras
2004-10-20
*
Nouvelle en-tête
herbelin
2004-07-16
*
ajout decimal_exp pour interpreter les notations decimales
mohring
2004-03-12
*
modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixes
barras
2003-12-15
*
power associe a droite
marche
2003-12-05
*
Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...
herbelin
2003-11-29
*
Restauration preference Rge a Rle pour compatibilite...
herbelin
2003-11-02
*
Notations pour l'exponentiation
herbelin
2003-10-13
*
Notation '^'
herbelin
2003-10-10
*
Ajout et MAJ commandes de scopes
herbelin
2003-09-12
*
Bug
herbelin
2003-05-21
*
Amelioration presentation
herbelin
2003-05-14
*
Amelioration affichage
herbelin
2003-05-14
*
Deplacement lemmes sur fact de Reals vers Arith
herbelin
2003-05-14
*
Open Scope en Local
herbelin
2003-04-12
*
Remplacement Import par Open Scope en v8
herbelin
2003-04-10
*
Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import".
herbelin
2003-04-09
*
*** empty log message ***
barras
2003-03-12
*
Restructuration des hints pour qu'Auto fasse moins de détours et les
herbelin
2003-02-27
*
Renommage de RealsB en Rbase
desmettr
2003-01-16
*
Réorganisation de la librairie des réels
desmettr
2002-11-27
*
Double Induction prend maintenant des noms d'hyppthèses
herbelin
2002-05-29
*
Uniformisation (Qed/Save et Implicits Arguments)
herbelin
2002-04-17
*
option -dump-glob pour coqdoc
filliatr
2002-02-14
*
Oubli Save + je sais plus
mayero
2001-06-19
*
Ajouts de lemmes (pour Float)
mayero
2001-06-18
*
Ajout de Rseries et Rtrigo_fun
mayero
2001-04-24
[next]