From 9938aed874d3e15e5d21689ea841bdc3e6ebb40e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 11 Jul 2017 21:51:23 +0200 Subject: Safer API for Global.body_of_constant and variants. We aditionally return the abstract universe context inside the option. This is relatively painless as most uses were using the option as a boolean. --- library/global.ml | 5 ++--- library/global.mli | 4 ++-- library/heads.ml | 2 +- 3 files changed, 5 insertions(+), 6 deletions(-) (limited to 'library') diff --git a/library/global.ml b/library/global.ml index cb6334c74..3a74f535d 100644 --- a/library/global.ml +++ b/library/global.ml @@ -126,9 +126,8 @@ let opaque_tables () = Environ.opaque_tables (env ()) let instantiate cb c = let open Declarations in match cb.const_universes with - | Monomorphic_const _ -> c - | Polymorphic_const ctx -> - Vars.subst_instance_constr (Univ.AUContext.instance ctx) c + | Monomorphic_const _ -> c, Univ.AUContext.empty + | Polymorphic_const ctx -> c, ctx let body_of_constant_body cb = let open Declarations in diff --git a/library/global.mli b/library/global.mli index d9190736f..d6d2f1f85 100644 --- a/library/global.mli +++ b/library/global.mli @@ -89,8 +89,8 @@ val constant_of_delta_kn : kernel_name -> constant val mind_of_delta_kn : kernel_name -> mutual_inductive val opaque_tables : unit -> Opaqueproof.opaquetab -val body_of_constant : constant -> Term.constr option -val body_of_constant_body : Declarations.constant_body -> Term.constr option +val body_of_constant : constant -> (Term.constr * Univ.AUContext.t) option +val body_of_constant_body : Declarations.constant_body -> (Term.constr * Univ.AUContext.t) option (** Global universe name <-> level mapping *) type universe_names = diff --git a/library/heads.ml b/library/heads.ml index a1cb81242..c12fa9479 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -132,7 +132,7 @@ let compute_head = function in (match body with | None -> RigidHead (RigidParameter cst) - | Some c -> kind_of_head env c) + | Some (c, _) -> kind_of_head env c) | EvalVarRef id -> (match Global.lookup_named id with | LocalDef (_,c,_) when not (Decls.variable_opacity id) -> -- cgit v1.2.3