diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2015-09-14 18:35:48 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2015-09-14 18:41:09 +0200 |
| commit | 2bc88f9a536c3db3c2d4a38a8a0da0500b895c7b (patch) | |
| tree | ce5b0fed1af0fb238a23d6b78a57a9bf2df29bb7 /tactics | |
| parent | 490160d25d3caac1d2ea5beebbbebc959b1b3832 (diff) | |
Univs: Add universe binding lists to definitions
... lemmas and inductives to control which universes are bound and where
in universe polymorphic definitions. Names stay outside the kernel.
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 749e0d2b5..e1c9c2de5 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 9a64b03fd..efd6ded44 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 719cc7c98..aa057a3e8 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 = |