aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-07-10 19:11:20 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-07-11 14:50:47 +0200
commit012f5fb722a9d5dcef82c800aa54ed50c0a58957 (patch)
treefbe0e3ae6901faba4f14b8cd4dbda019ce9a7829 /pretyping
parentb8a7222e670f69e024d50394afd88204e15d1b29 (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 'pretyping')
-rw-r--r--pretyping/recordops.ml5
-rw-r--r--pretyping/typeclasses.ml4
-rw-r--r--pretyping/vnorm.ml4
3 files changed, 7 insertions, 6 deletions
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 1cb694da6..9fc2573ac 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -198,7 +198,8 @@ let warn_projection_no_head_constant =
let compute_canonical_projections warn (con,ind) =
let env = Global.env () in
let ctx = Environ.constant_context env con 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 v = (mkConstU (con,u)) in
let ctx = Univ.ContextSet.of_context ctx in
let c = Environ.constant_value_in env (con,u) in
@@ -298,7 +299,7 @@ let error_not_structure ref =
let check_and_decompose_canonical_structure ref =
let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref in
let env = Global.env () in
- let u = Environ.constant_instance env sp in
+ let u = Univ.AUContext.instance (Environ.constant_context env sp) in
let vc = match Environ.constant_opt_value_in env (sp, u) with
| Some vc -> vc
| None -> error_not_structure ref in
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 201f79c39..bae831b63 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -117,10 +117,10 @@ let typeclass_univ_instance (cl,u') =
match cl.cl_impl with
| ConstRef c ->
let cb = Global.lookup_constant c in
- Declareops.constant_polymorphic_instance cb
+ Univ.AUContext.instance (Declareops.constant_polymorphic_context cb)
| IndRef c ->
let mib,oib = Global.lookup_inductive c in
- Declareops.inductive_polymorphic_instance mib
+ Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib)
| _ -> Univ.Instance.empty
in Array.fold_left2 (fun subst u u' -> Univ.LMap.add u u' subst)
Univ.LMap.empty (Univ.Instance.to_array u) (Univ.Instance.to_array u')
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index b3eaa3cb9..66cc42cb6 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -174,7 +174,7 @@ and nf_whd env sigma whd typ =
| Vatom_stk(Aind ((mi,i) as ind), stk) ->
let mib = Environ.lookup_mind mi env in
let nb_univs =
- Univ.Instance.length (Declareops.inductive_polymorphic_instance mib)
+ Univ.AUContext.size (Declareops.inductive_polymorphic_context mib)
in
let mk u =
let pind = (ind, u) in (mkIndU pind, type_of_ind env pind)
@@ -203,7 +203,7 @@ and constr_type_of_idkey env sigma (idkey : Vars.id_key) stk =
| ConstKey cst ->
let cbody = Environ.lookup_constant cst env in
let nb_univs =
- Univ.Instance.length (Declareops.constant_polymorphic_instance cbody)
+ Univ.AUContext.size (Declareops.constant_polymorphic_context cbody)
in
let mk u =
let pcst = (cst, u) in (mkConstU pcst, Typeops.type_of_constant_in env pcst)