From 25ef9dda0311213bb2f6e2b9cd0b87be2128599b Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 25 Jul 2016 15:44:53 +0200 Subject: Fix #4769, univ poly and elim schemes in sections --- tactics/elimschemes.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'tactics/elimschemes.ml') diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 4ff774b8e..ba23568af 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -51,19 +51,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 = -- cgit v1.2.3