diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-11 17:16:18 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-13 15:14:45 +0200 |
| commit | 603bfb392805fb8d1559d304bcf1b9c7b938bb6e (patch) | |
| tree | 37dde8996de9a02c03d518c69120b44827d4bc21 /pretyping | |
| parent | e3eb17a728d7b6874e67462e8a83fac436441872 (diff) | |
Getting rid of AUContext abstraction breakers in Recordops.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 3 | ||||
| -rw-r--r-- | pretyping/recordops.ml | 8 | ||||
| -rw-r--r-- | pretyping/recordops.mli | 2 |
3 files changed, 6 insertions, 7 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 87f29ba49..cb76df4e8 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -205,7 +205,8 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = else match (Stack.strip_n_app (l_us-1) sk2_effective) with | None -> raise Not_found | Some (l',el,s') -> (l'@Stack.append_app [|el|] Stack.empty,s') in - let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in + let u, ctx' = Universes.fresh_instance_from ctx None in + let subst = Univ.make_inverse_instance_subst u in let c = EConstr.of_constr c in let c' = subst_univs_level_constr subst c in let t' = EConstr.of_constr t' in 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 diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 27d1650af..de09edcdc 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -57,7 +57,7 @@ type cs_pattern = type obj_typ = { o_DEF : constr; - o_CTX : Univ.ContextSet.t; + o_CTX : Univ.AUContext.t; o_INJ : int option; (** position of trivial argument *) o_TABS : constr list; (** ordered *) o_TPARAMS : constr list; (** ordered *) |