diff options
Diffstat (limited to 'tactics/elimschemes.ml')
| -rw-r--r-- | tactics/elimschemes.ml | 21 |
1 files changed, 14 insertions, 7 deletions
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 4ff774b8..93073fdc 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -18,6 +18,7 @@ open Indrec open Declarations open Typeops open Ind_tables +open Sigma.Notations (* Induction/recursion schemes *) @@ -51,19 +52,21 @@ let optimize_non_type_induction_scheme kind dep sort _ ind = let u = Univ.UContext.instance ctx in let ctxset = Univ.ContextSet.of_context ctx in let ectx = Evd.evar_universe_context_of ctxset in - let sigma, c = build_induction_scheme env (Evd.from_ctx ectx) (ind,u) dep sort in + let sigma = Evd.merge_universe_context sigma ectx in + let sigma, c = build_induction_scheme env sigma (ind,u) dep sort in (c, Evd.evar_universe_context sigma), Safe_typing.empty_private_constants let build_induction_scheme_in_type dep sort ind = let env = Global.env () in + let sigma = Evd.from_env env in let ctx = let mib,mip = Inductive.lookup_mind_specif env ind in Declareops.inductive_context mib in let u = Univ.UContext.instance ctx in let ctxset = Univ.ContextSet.of_context ctx in - let ectx = Evd.evar_universe_context_of ctxset in - let sigma, c = build_induction_scheme env (Evd.from_ctx ectx) (ind,u) dep sort in + let sigma = Evd.merge_universe_context sigma (Evd.evar_universe_context_of ctxset) in + let sigma, c = build_induction_scheme env sigma (ind,u) dep sort in c, Evd.evar_universe_context sigma let rect_scheme_kind_from_type = @@ -94,6 +97,10 @@ let rec_scheme_kind_from_prop = declare_individual_scheme_object "_rec" ~aux:"_rec_from_prop" (optimize_non_type_induction_scheme rect_scheme_kind_from_prop false InSet) +let rec_scheme_kind_from_type = + declare_individual_scheme_object "_rec_nodep" ~aux:"_rec_nodep_from_type" + (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InSet) + let rec_dep_scheme_kind_from_type = declare_individual_scheme_object "_rec" ~aux:"_rec_from_type" (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_type true InSet) @@ -102,10 +109,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 = 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 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 case_scheme_kind_from_type = declare_individual_scheme_object "_case_nodep" |