diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-07-13 15:05:48 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-07-13 15:05:48 +0200 |
| commit | e3eb17a728d7b6874e67462e8a83fac436441872 (patch) | |
| tree | c7932e27be16f4d2c20da8d61c3a61b101be7f70 /pretyping/recordops.ml | |
| parent | 9427b99b167842bc4a831def815c4824030d518f (diff) | |
| parent | 95d65ae4ec8c01f0b8381dfa7029bb32a552bcb0 (diff) | |
Merge PR #870: Prepare De Bruijn universe abstractions, Episode I: 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 4131f9a61..c498089ca 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -203,7 +203,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 @@ -301,7 +302,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 |