diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-11 21:51:23 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-13 15:14:45 +0200 |
commit | 9938aed874d3e15e5d21689ea841bdc3e6ebb40e (patch) | |
tree | f3c08864d8e26e29350d541904412cc07da79abf /library | |
parent | 001c95411b6674423886a085d8f624ea031a9ebc (diff) |
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.
Diffstat (limited to 'library')
-rw-r--r-- | library/global.ml | 5 | ||||
-rw-r--r-- | library/global.mli | 4 | ||||
-rw-r--r-- | library/heads.ml | 2 |
3 files changed, 5 insertions, 6 deletions
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) -> |