diff options
| author | Guillaume Melquiond | 2016-08-24 06:59:19 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2016-08-24 06:59:19 +0200 |
| commit | 433d042350f7d7e52f9ef5def0f9405218cb109b (patch) | |
| tree | f07c4afe0962a8aa9c841264da0c0c3cf9fc06f6 | |
| parent | 96feefe1deef3486055836ef68ba8150f32d7593 (diff) | |
Properly compute types for assumed section variables (bug #5035).
This bug was introduced by
commit 34ef02fac1110673ae74c41c185c228ff7876de2
Author: Matej Kosik <m4tej.kosik@gmail.com>
Date: Fri Jan 29 10:13:12 2016 +0100
CLEANUP: Context.{Rel,Named}.Declaration.t
| -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 |