diff options
| author | Pierre-Marie Pédrot | 2020-05-14 13:58:23 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-07-22 12:46:20 +0200 |
| commit | 675b23dcf824d8a851881171a5628b239aad2201 (patch) | |
| tree | 90b800d6524b93c23c0adc6e0a941db7f421cc79 /test-suite | |
| parent | e6d92a9765f84c80f8c6a102fe5480490c747313 (diff) | |
Remove redundant data from VM case switch.
No need to store the case_info, all the data is reconstructible from the
context. Furthermore, this reconstruction is performed in a context where
we already access the environment, so performance is not at stake.
Hopefully this will also reduce the number of globally allocated VM values,
since the switch representation now only depends on the shape of the inductive
type.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/sprop.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/test-suite/success/sprop.v b/test-suite/success/sprop.v index d3e2749088..3a6dfb1e11 100644 --- a/test-suite/success/sprop.v +++ b/test-suite/success/sprop.v @@ -171,6 +171,10 @@ End sFix. Fail Definition fix_relevance : _ -> nat := fun _ : iUnit => 0. +(* Check that VM/native properly keep the relevance of the predicate in the case info + (bad-relevance warning as error otherwise) *) +Definition vm_rebuild_case := Eval vm_compute in eq_sind. + Require Import ssreflect. Goal forall T : SProp, T -> True. |