From 603bfb392805fb8d1559d304bcf1b9c7b938bb6e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 11 Jul 2017 17:16:18 +0200 Subject: Getting rid of AUContext abstraction breakers in Recordops. --- pretyping/recordops.ml | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) (limited to 'pretyping/recordops.ml') diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index c498089ca..a23579609 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -134,7 +134,7 @@ let find_projection = function type obj_typ = { o_DEF : constr; - o_CTX : Univ.ContextSet.t; + o_CTX : Univ.AUContext.t; o_INJ : int option; (* position of trivial argument if any *) o_TABS : constr list; (* ordered *) o_TPARAMS : constr list; (* ordered *) @@ -203,10 +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.AUContext.instance ctx in - let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in + let u = Univ.make_abstract_instance 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 let sign,t = Reductionops.splay_lam env Evd.empty (EConstr.of_constr c) in let t = EConstr.Unsafe.to_constr t in @@ -302,7 +300,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 = Univ.AUContext.instance (Environ.constant_context env sp) in + let u = Univ.make_abstract_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 -- cgit v1.2.3