diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-12 14:32:55 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-13 15:14:45 +0200 |
| commit | 1014de55656c2698500089d940a12f7e4b26a0de (patch) | |
| tree | ea204cc60782b6f6bff35f9aa3515ae7751c2985 | |
| parent | fb49af8874d01871ea7ca0bd2a46d135dba27bc2 (diff) | |
Getting rid of AUContext abstraction breakers in Elimschemes.
| -rw-r--r-- | tactics/elimschemes.ml | 21 |
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 = |