diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-12-15 23:15:02 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-12-15 23:15:02 +0100 |
| commit | 33742251e62a49c7996b96ca7077cf985627d14b (patch) | |
| tree | e75d9166f963fdfa21ab754e2c9471909143ac60 /test-suite/success/proof_using.v | |
| parent | 7212e6c4a742110138a268650a59a67ef28d0582 (diff) | |
Proof using: do not clear unused section hyps automatically
The option is still there, but not documented since it is too
dangerous. Hints and type classes instances are not taking cleared
variables into account.
Diffstat (limited to 'test-suite/success/proof_using.v')
| -rw-r--r-- | test-suite/success/proof_using.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/test-suite/success/proof_using.v b/test-suite/success/proof_using.v index c83f45e2a..adaa05ad0 100644 --- a/test-suite/success/proof_using.v +++ b/test-suite/success/proof_using.v @@ -178,6 +178,7 @@ End Let. Check (test_let 3). +(* Disabled Section Clear. Variable a: nat. @@ -192,6 +193,6 @@ trivial. Qed. End Clear. - +*) |