diff options
Diffstat (limited to 'tactics/eqschemes.ml')
| -rw-r--r-- | tactics/eqschemes.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 507ff10ee..efcefcf16 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -57,7 +57,6 @@ open Namegen open Inductiveops open Ind_tables open Indrec -open Sigma.Notations open Context.Rel.Declaration module RelDecl = Context.Rel.Declaration @@ -656,10 +655,10 @@ let fix_r2l_forward_rew_scheme (c, ctx') = (**********************************************************************) let build_r2l_rew_scheme dep env ind k = - let sigma = Sigma.Unsafe.of_evar_map (Evd.from_env env) in - let Sigma (indu, sigma, _) = Sigma.fresh_inductive_instance env sigma ind in - let Sigma (c, sigma, _) = build_case_analysis_scheme env sigma indu dep k in - c, Evd.evar_universe_context (Sigma.to_evar_map sigma) + let sigma = Evd.from_env env in + let (sigma, indu) = Evd.fresh_inductive_instance env sigma ind in + let (sigma, c) = build_case_analysis_scheme env sigma indu dep k in + c, Evd.evar_universe_context sigma let build_l2r_rew_scheme = build_l2r_rew_scheme let build_l2r_forward_rew_scheme = build_l2r_forward_rew_scheme |