diff options
| -rw-r--r-- | toplevel/assumptions.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml index 30b7f299f8..45c539e229 100644 --- a/toplevel/assumptions.ml +++ b/toplevel/assumptions.ml @@ -283,7 +283,9 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = let fold obj _ accu = match obj with | VarRef id -> let decl = Global.lookup_named id in - if is_local_assum decl then ContextObjectMap.add (Variable id) t accu + if is_local_assum decl then + let t = Context.Named.Declaration.get_type decl in + ContextObjectMap.add (Variable id) t accu else accu | ConstRef kn -> let cb = lookup_constant kn in |