aboutsummaryrefslogtreecommitdiff
path: root/theories/Reals
AgeCommit message (Expand)Author
2017-02-15Added some theory on powerRZ.Thomas Sibut-Pinote
2016-10-24Remove v62 from stdlib.Théo Zimmermann
2016-08-18Fix an occurrence of deprecated eqn syntax in stdlib.Maxime Dénès
2016-06-03Removing "intro" from the tactic AST.Pierre-Marie Pédrot
2016-04-27Revert "Temporary hack to compensate missing comma while re-printing tactic"Hugo Herbelin
2016-04-27Temporary hack to compensate missing comma while re-printing tacticHugo Herbelin
2016-03-04Making parentheses mandatory in tactic scopes.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-07-31Remove some outdated files and fix permissions.Guillaume Melquiond
2015-04-01Accomodating #4166 (providing "Require Import OmegaTactic" as aHugo Herbelin
2015-03-06Add some missing Proof keywords.Guillaume Melquiond
2015-01-12Update headers.Maxime Dénès
2014-09-27Keyed unification option, compiling the whole standard libraryMatthieu Sozeau
2014-09-23adds general facts in the Reals library, whose need was detected inYves Bertot
2014-09-17Change some Defined into Qed.Guillaume Melquiond
2014-09-17Add some missing Proof statements.Guillaume Melquiond
2014-09-17Change an axiom into a definition.Guillaume Melquiond
2014-08-05More proofs independent of the names generated by induction/elim overHugo Herbelin
2014-06-26Deactivate the "Standard Propositions Naming" flag, source of a lot ofHugo Herbelin
2014-06-04Make standard library independent of the names generated byHugo Herbelin
2014-06-04Make standard library independent of the names generated byHugo Herbelin
2014-06-04Remove spurious Show in script.Matthieu Sozeau
2014-06-01Making those proofs which depend on names generated for the argumentsHugo Herbelin
2014-05-12Now parsing rules of ML-declared tactics are only made available after thePierre-Marie Pédrot
2014-05-06Correct rebase on STM code. Thanks to E. Tassi for help on dealing withMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-23Import proof of decidability of negated formulas from Coquelicot.Guillaume Melquiond
2014-04-22Remove some uses of excluded middle.Guillaume Melquiond
2014-04-22Replace the proof of sig_forall_dec from Kaliszyk/O'Connor by the one from Co...Guillaume Melquiond
2014-04-16Fixing missing headers.Hugo Herbelin
2014-04-10No more Coersion in Init.Pierre Boutillier
2014-03-10Add missing lemmas: Rplus_eq_compat_r and Rplus_eq_reg_r.Guillaume Melquiond
2013-12-04Add lemma derivable_pt_lim_atan.Guillaume Melquiond
2013-12-03Fix statement of Rplus_lt_reg_r and add Rplus_lt_reg_l.Guillaume Melquiond
2013-12-03Remove a useless hypothesis from Rle_Rinv.Guillaume Melquiond
2013-01-18Unset Asymmetric Patternspboutill
2012-10-26Change Hint Resolve, Immediate to take a global reference as argumentmsozeau
2012-10-16Removing redundant definition of case_eq (see #2919).herbelin
2012-08-08Updating headers.herbelin
2012-07-05Legacy Ring and Legacy Field migrated to contribsletouzey
2012-07-05Some cleanup in recent proofs concerning piletouzey
2012-07-05Kills the useless tactic annotations "in |- *"letouzey
2012-07-05Open Local Scope ---> Local Open Scope, same with Notation and aliiletouzey
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2012-06-11These files are displaced from Rtrigo.v and Ranalysis_reg.vbertot
2012-06-11finish the rearrangement for removing the sin_PI2 axiom. This new versionbertot
2012-06-11Adds the proof of PI_ineq, plus some other smarter ways to approximate PIbertot
2012-06-05Modifications and rearrangements to remove the action that sin (PI/2) = 1bertot
2012-04-15Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).herbelin
2011-11-21theories/, plugins/ and test-suite/ ported to the Arguments vernaculargareuselesinge
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 12:35:21 +0000