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 /tactics/eqschemes.mli | |
| 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 'tactics/eqschemes.mli')
| -rw-r--r-- | tactics/eqschemes.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/eqschemes.mli b/tactics/eqschemes.mli index d1038f2655..6447708ace 100644 --- a/tactics/eqschemes.mli +++ b/tactics/eqschemes.mli @@ -27,7 +27,7 @@ val rew_r2l_scheme_kind : individual scheme_kind val build_r2l_rew_scheme : bool -> env -> inductive -> Sorts.family -> constr Evd.in_evar_universe_context val build_l2r_rew_scheme : bool -> env -> inductive -> Sorts.family -> - constr Evd.in_evar_universe_context * Evd.side_effects + constr Evd.in_evar_universe_context val build_r2l_forward_rew_scheme : bool -> env -> inductive -> Sorts.family -> constr Evd.in_evar_universe_context val build_l2r_forward_rew_scheme : @@ -39,7 +39,7 @@ val build_sym_scheme : env -> inductive -> constr Evd.in_evar_universe_context val sym_scheme_kind : individual scheme_kind val build_sym_involutive_scheme : env -> inductive -> - constr Evd.in_evar_universe_context * Evd.side_effects + constr Evd.in_evar_universe_context val sym_involutive_scheme_kind : individual scheme_kind (** Builds a congruence scheme for an equality type *) |