diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-03-05 13:40:18 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-03-06 10:48:42 +0100 |
| commit | fe902cb9235a29427f18c234ffffc9b9070512a1 (patch) | |
| tree | 55801193852b70d97521874f3f351d0f867cb05f /test-suite/success | |
| parent | db8fcbb7763ac784f7c72b72509d5dc7c2c5323c (diff) | |
[compat] Remove "Shrink Abstract"
Following up on #6791, we the option "Shrink Abstract".
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/shrink_abstract.v | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/test-suite/success/shrink_abstract.v b/test-suite/success/shrink_abstract.v index 3f6b9cb39..916bb846a 100644 --- a/test-suite/success/shrink_abstract.v +++ b/test-suite/success/shrink_abstract.v @@ -1,5 +1,3 @@ -Set Shrink Abstract. - Definition foo : forall (n m : nat), bool. Proof. pose (p := 0). |