aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-05-08 18:36:34 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-05-31 19:10:08 +0200
commit979e48bfe1a16b0cbc6671a78297d496b730bf99 (patch)
treeccdcdb0e8ffbb0969bd54d3d5b52da43c15ee6c0 /theories/Reals
parent1aaee2d7f0934b625215c259fa207ce96977b0f6 (diff)
Upgrade Matthieu's new_revert as the "revert" (a "unit tactic").
Diffstat (limited to 'theories/Reals')
0 files changed, 0 insertions, 0 deletions