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/Ranalysis3.v | |
| parent | 1aaee2d7f0934b625215c259fa207ce96977b0f6 (diff) | |
Upgrade Matthieu's new_revert as the "revert" (a "unit tactic").
Diffstat (limited to 'theories/Reals/Ranalysis3.v')
0 files changed, 0 insertions, 0 deletions