diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/elimschemes.ml | 4 | ||||
| -rw-r--r-- | tactics/leminv.ml | 2 | ||||
| -rw-r--r-- | tactics/rewrite.ml | 4 |
3 files changed, 5 insertions, 5 deletions
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 749e0d2b5b..e1c9c2de59 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -51,7 +51,7 @@ 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_env ~ctx:ectx env) (ind,u) dep sort in + let sigma, c = build_induction_scheme env (Evd.from_ctx ectx) (ind,u) dep sort in (c, Evd.evar_universe_context sigma), Declareops.no_seff let build_induction_scheme_in_type dep sort ind = @@ -63,7 +63,7 @@ let build_induction_scheme_in_type 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_env ~ctx:ectx env) (ind,u) dep sort in + let sigma, c = build_induction_scheme env (Evd.from_ctx ectx) (ind,u) dep sort in c, Evd.evar_universe_context sigma let rect_scheme_kind_from_type = diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 9a64b03fd1..efd6ded44c 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -194,7 +194,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = errorlabstrm "lemma_inversion" (str"Computed inversion goal was not closed in initial signature."); *) - let pf = Proof.start (Evd.from_env ~ctx:(evar_universe_context sigma) invEnv) [invEnv,invGoal] in + let pf = Proof.start (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in let pf = fst (Proof.run_tactic env ( tclTHEN intro (onLastHypId inv_op)) pf) diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 719cc7c98d..aa057a3e86 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1824,8 +1824,8 @@ let declare_projection n instance_id r = let build_morphism_signature m = let env = Global.env () in - let m,ctx = Constrintern.interp_constr env Evd.empty m in - let sigma = Evd.from_env ~ctx env in + let m,ctx = Constrintern.interp_constr env (Evd.from_env env) m in + let sigma = Evd.from_ctx ctx in let t = Typing.unsafe_type_of env sigma m in let cstrs = let rec aux t = |