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 /pretyping/recordops.ml | |
| 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 'pretyping/recordops.ml')
| -rw-r--r-- | pretyping/recordops.ml | 5 |
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 |