diff options
| author | Pierre-Marie Pédrot | 2020-04-21 17:26:11 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-04-28 16:31:07 +0200 |
| commit | 2c04f5df480492169e533c376cc50caff863ba5a (patch) | |
| tree | 99a46c1bd61d4e81b14981d66f69d5822d88b1bf /test-suite | |
| parent | 196b5e0d10db966529b3bd1d27014a9742c71d7c (diff) | |
Stop relying on side-effects for recursive scheme declaration.
Instead, we register functions dynamically declaring the dependencies of the
scheme to be generated.
We had to fix the test-suite because an internal scheme name changed.
We could also tweak the internal flag of scheme dependencies, but in this
particular case it looks more like a bug from the previous implementation.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/Scheme.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/Scheme.v b/test-suite/success/Scheme.v index 4b928007cf..273cb48295 100644 --- a/test-suite/success/Scheme.v +++ b/test-suite/success/Scheme.v @@ -18,7 +18,7 @@ Check myeq_rew. Check myeq_rew_dep. Check myeq_rew_fwd_dep. Check myeq_rew_r. -Check internal_myeq_sym_involutive. +Check myeq_sym_involutive. Check myeq_rew_r_dep. Check myeq_rew_fwd_r_dep. |