From bb774b704c45ee182669e133115ea606d595a004 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 6 Apr 2011 16:48:55 +0000
Subject: Fix dev/base_include after change of constant_body

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

(limited to 'dev/base_include')

diff --git a/dev/base_include b/dev/base_include
index 18c5c324a..5d5e9e1dc 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -189,7 +189,7 @@ open Declarations;;
 
 let constbody_of_string s =
   let b = Global.lookup_constant (Nametab.locate_constant (qualid_of_string s)) in
-  Option.get b.const_body;;
+  Option.get (body_of_constant b);;
 
 (* Get the current goal *)
 (*
-- 
cgit v1.2.3