aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals/Rlogic.v
Commit message (Expand)AuthorAge
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* Import proof of decidability of negated formulas from Coquelicot.Gravatar Guillaume Melquiond2014-04-23
* Replace the proof of sig_forall_dec from Kaliszyk/O'Connor by the one from Co...Gravatar Guillaume Melquiond2014-04-22
* Updating headers.Gravatar herbelin2012-08-08
* Kills the useless tactic annotations "in |- *"Gravatar letouzey2012-07-05
* Cleaning a little bit the files talking about descriptions: avoidingGravatar herbelin2011-11-03
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'Gravatar letouzey2009-10-08
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Take advantage of natdynlink when available: almost all contribs become loada...Gravatar letouzey2008-12-16
* Commit d'une preuve de l'axiome d'Archimède qui traînait dans mes placards.Gravatar herbelin2008-03-23
* Une passe sur les réels:Gravatar herbelin2008-03-23
* Nicer proofs.Gravatar roconnor2008-01-24
* remove Fourier Failure warnings.Gravatar roconnor2008-01-24
* Prove the decidability of arithmetical statements using the real numbers.Gravatar roconnor2008-01-24
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-02 09:56:05 +0000