From 433d042350f7d7e52f9ef5def0f9405218cb109b Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 24 Aug 2016 06:59:19 +0200
Subject: 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
---
 toplevel/assumptions.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

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
-- 
cgit v1.2.3