diff options
Diffstat (limited to 'tactics/elimschemes.ml')
| -rw-r--r-- | tactics/elimschemes.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 93073fdc7..466b1350d 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -18,7 +18,6 @@ open Indrec open Declarations open Typeops open Ind_tables -open Sigma.Notations (* Induction/recursion schemes *) @@ -109,10 +108,10 @@ let rec_dep_scheme_kind_from_type = let build_case_analysis_scheme_in_type dep sort ind = let env = Global.env () in - 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 sort 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 sort in + c, Evd.evar_universe_context sigma let case_scheme_kind_from_type = declare_individual_scheme_object "_case_nodep" |