diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-10 19:11:20 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-11 14:50:47 +0200 |
| commit | 012f5fb722a9d5dcef82c800aa54ed50c0a58957 (patch) | |
| tree | fbe0e3ae6901faba4f14b8cd4dbda019ce9a7829 /tactics | |
| parent | b8a7222e670f69e024d50394afd88204e15d1b29 (diff) | |
Safe API for accessing universe constraints of global references.
Instead of returning either an instance or the set of constraints, we rather
return the corresponding abstracted context. We also push back all uses of
abstraction-breaking calls from these functions out of the kernel.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/elimschemes.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 5d9d36958..e058806a3 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -48,7 +48,8 @@ let optimize_non_type_induction_scheme kind dep sort _ ind = else let mib,mip = Inductive.lookup_mind_specif env ind in let ctx = Declareops.inductive_polymorphic_context mib in - let u = Univ.UContext.instance ctx 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 @@ -62,7 +63,8 @@ let build_induction_scheme_in_type dep sort ind = let mib,mip = Inductive.lookup_mind_specif env ind in Declareops.inductive_polymorphic_context mib in - let u = Univ.UContext.instance ctx 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 |