diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/global.ml | 3 | ||||
| -rw-r--r-- | library/global.mli | 2 | ||||
| -rw-r--r-- | library/heads.ml | 2 |
3 files changed, 6 insertions, 1 deletions
diff --git a/library/global.ml b/library/global.ml index 6083c40794..dcb20a280e 100644 --- a/library/global.ml +++ b/library/global.ml @@ -259,6 +259,9 @@ let is_type_in_type r = | IndRef ind -> Environ.type_in_type_ind ind env | ConstructRef cstr -> Environ.type_in_type_ind (inductive_of_constructor cstr) env +let current_modpath () = + Safe_typing.current_modpath (safe_env ()) + let current_dirpath () = Safe_typing.current_dirpath (safe_env ()) diff --git a/library/global.mli b/library/global.mli index 906d246eef..57e173cb93 100644 --- a/library/global.mli +++ b/library/global.mli @@ -157,6 +157,8 @@ val set_strategy : Constant.t Names.tableKey -> Conv_oracle.level -> unit (* Modifies the global state, registering new universes *) +val current_modpath : unit -> ModPath.t + val current_dirpath : unit -> DirPath.t val with_global : (Environ.env -> DirPath.t -> 'a Univ.in_universe_context_set) -> 'a diff --git a/library/heads.ml b/library/heads.ml index 3d5f6a6ff0..d9d650ac07 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -129,7 +129,7 @@ let compute_head = function let cb = Environ.lookup_constant cst env in let is_Def = function Declarations.Def _ -> true | _ -> false in let body = - if not cb.Declarations.const_proj && is_Def cb.Declarations.const_body + if not (Environ.is_projection cst env) && is_Def cb.Declarations.const_body then Global.body_of_constant cst else None in (match body with |