aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/search.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/search.ml')
-rw-r--r--vernac/search.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/search.ml b/vernac/search.ml
index 5cf6a9491..0f56f81e7 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -78,7 +78,7 @@ let iter_declarations (fn : global_reference -> env -> constr -> unit) =
| "CONSTANT" ->
let cst = Global.constant_of_delta_kn kn in
let gr = ConstRef cst in
- let typ = Global.type_of_global_unsafe gr in
+ let (typ, _) = Global.type_of_global_in_context (Global.env ()) gr in
fn gr env typ
| "INDUCTIVE" ->
let mind = Global.mind_of_delta_kn kn in