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/elimschemes.ml | |
| 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/elimschemes.ml')
| -rw-r--r-- | tactics/elimschemes.ml | 4 |
1 files changed, 2 insertions, 2 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 = |