diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-05-08 18:36:34 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-05-31 19:10:08 +0200 |
commit | 979e48bfe1a16b0cbc6671a78297d496b730bf99 (patch) | |
tree | ccdcdb0e8ffbb0969bd54d3d5b52da43c15ee6c0 /theories/Reals | |
parent | 1aaee2d7f0934b625215c259fa207ce96977b0f6 (diff) |
Upgrade Matthieu's new_revert as the "revert" (a "unit tactic").
Diffstat (limited to 'theories/Reals')
0 files changed, 0 insertions, 0 deletions