diff options
author | Matthieu Sozeau <mattam@mattam.org> | 2016-07-29 19:41:46 +0200 |
---|---|---|
committer | Matthieu Sozeau <mattam@mattam.org> | 2016-07-29 19:41:46 +0200 |
commit | dabe6d0e1d1782d3e9647e04aa1bf161765ad882 (patch) | |
tree | e0ac77d200c301b08e2f0532993de6d6e3ab1862 /tactics | |
parent | 81c19bdd631fa72afa0cac5c8b915d836e0646df (diff) | |
parent | 639eecd27e42c7dd646afdcb67b5a4e51a4541c1 (diff) |
Merge remote-tracking branch 'gforge/v8.5' into v8.6
Diffstat (limited to 'tactics')
-rw-r--r-- | tactics/elimschemes.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 99c2d8210..93073fdc7 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -52,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 = |