From 24f8331a3bc9631c37f162826514e6cb7d679a16 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sun, 4 Nov 2007 13:10:56 +0000
Subject: Fix bug#1739

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10286 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/subtac/subtac_obligations.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 941a7576e8..769aff9dcf 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -135,7 +135,7 @@ let declare_definition prg =
      with _ -> ());
   let ce = 
     { const_entry_body = body;
-      const_entry_type = Some prg.prg_type;
+      const_entry_type = Some (Termops.refresh_universes prg.prg_type);
       const_entry_opaque = false;
       const_entry_boxed = false} 
   in
-- 
cgit v1.2.3