aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/assumptions.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/assumptions.ml')
-rw-r--r--library/assumptions.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/library/assumptions.ml b/library/assumptions.ml
index 9cfe531ce..37585caa4 100644
--- a/library/assumptions.ml
+++ b/library/assumptions.ml
@@ -222,7 +222,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st (* t *) =
and add_kn kn s acc =
let cb = lookup_constant kn in
let do_type cst =
- let ctype = cb.Declarations.const_type in
+ let ctype = Global.type_of_global_unsafe (Globnames.ConstRef kn) in
(s,ContextObjectMap.add cst ctype acc)
in
let (s,acc) =