aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-07-12 14:32:55 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-07-13 15:14:45 +0200
commit1014de55656c2698500089d940a12f7e4b26a0de (patch)
treeea204cc60782b6f6bff35f9aa3515ae7751c2985
parentfb49af8874d01871ea7ca0bd2a46d135dba27bc2 (diff)
Getting rid of AUContext abstraction breakers in Elimschemes.
-rw-r--r--tactics/elimschemes.ml21
1 files changed, 4 insertions, 17 deletions
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index e058806a3..2d2a0c1b2 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -46,28 +46,15 @@ let optimize_non_type_induction_scheme kind dep sort _ ind =
let sigma, nf = Evarutil.nf_evars_and_universes sigma in
(nf c', Evd.evar_universe_context sigma), eff
else
- let mib,mip = Inductive.lookup_mind_specif env ind in
- let ctx = Declareops.inductive_polymorphic_context mib in
- let u = Univ.AUContext.instance ctx in
- let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in
- let ctxset = Univ.ContextSet.of_context ctx in
- let ectx = Evd.evar_universe_context_of ctxset in
- let sigma = Evd.merge_universe_context sigma ectx in
- let sigma, c = build_induction_scheme env sigma (ind,u) dep sort in
+ let sigma, pind = Evd.fresh_inductive_instance env sigma ind in
+ let sigma, c = build_induction_scheme env sigma pind 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_polymorphic_context mib
- in
- let u = Univ.AUContext.instance ctx in
- let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in
- let ctxset = Univ.ContextSet.of_context ctx 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
+ let sigma, pind = Evd.fresh_inductive_instance env sigma ind in
+ let sigma, c = build_induction_scheme env sigma pind dep sort in
c, Evd.evar_universe_context sigma
let rect_scheme_kind_from_type =