aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/recordops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/recordops.ml')
-rw-r--r--pretyping/recordops.ml5
1 files changed, 3 insertions, 2 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