aboutsummaryrefslogtreecommitdiff
path: root/theories/Reals/Rtrigo.v
AgeCommit message (Expand)Author
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2018-07-17Remove fourier pluginMaxime Dénès
2018-02-27Update headers following #6543.Théo Zimmermann
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-06-01Making those proofs which depend on names generated for the argumentsHugo Herbelin
2014-04-22Remove some uses of excluded middle.Guillaume Melquiond
2012-08-08Updating headers.herbelin
2012-06-11finish the rearrangement for removing the sin_PI2 axiom. This new versionbertot
2012-06-05Modifications and rearrangements to remove the action that sin (PI/2) = 1bertot
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-02-18Removed Rtrigo's dependency on Classical.gmelquio
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-03-17- gros commit sur ring et field: passage des arguments simplifiebarras
2006-12-15Changement dans ring et field, beaucoup de correction d'erreurs,bgregoir
2006-12-11Changement dans le kernel : bgregoir
2006-10-17Mise en forme des theoriesnotin
2006-09-26mise a jour du nouveau ring et ajout du nouveau field, avant renommagesbarras
2004-10-20COMMITED BYTECODE COMPILERbarras
2004-07-16Nouvelle en-têteherbelin
2003-12-24changement de pose en set (pose n'etait pas utilise avec la semantiquebarras
2003-12-15modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixesbarras
2003-11-29Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...herbelin
2003-09-12Ajout et MAJ commandes de scopesherbelin
2003-05-14Amelioration presentationherbelin
2003-04-12Open Scope en Localherbelin
2003-04-10Remplacement Import par Open Scope en v8herbelin
2003-04-09Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import".herbelin
2003-03-12*** empty log message ***barras
2003-01-22Renommages dans Rtrigo_defdesmettr
2003-01-21Suppression de INR2 / Conséquence logique de la nouvelle représentation des...desmettr
2003-01-16Renommage de RealsB en Rbasedesmettr
2003-01-15Nouvelle interprétation des nombres réelsdesmettr
2002-11-27Réorganisation de la librairie des réelsdesmettr
2002-07-16*** empty log message ***desmettr
2002-07-16*** empty log message ***desmettr
2002-07-16MAJ Rtrigo pour sqrtdesmettr
2002-07-12cos_plus prouvedesmettr
2002-07-05sin_plus prouve (a partir de cos_plus)desmettr
2002-07-05sin_bound et cos_bound deplaces dans Rtrigo_altdesmettr
2002-07-03*** empty log message ***desmettr
2002-07-03sin_eq_0 est maintenant prouvedesmettr
2002-07-02sin_lb_gt_0 est maintenant prouve (grace a une approximation de PI, cf PI_ineq)desmettr
2002-07-02Suppression de l'axiome arc_sin_cosdesmettr
2002-07-02*** empty log message ***desmettr
2002-07-01Modification sin_approxdesmettr
2002-06-21Export Sumbool dans ProbBool; Reals charge et exporte ZArith_base seulementfilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:17:07 +0000