From 7306ee7c3027983da38dde0ae7aa85c46bc943f6 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 10 May 2001 13:01:47 +0000
Subject: ajout d'un afficher de contexte et d'une fonction constbody_of_string

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

(limited to 'dev/base_include')

diff --git a/dev/base_include b/dev/base_include
index 3001a5be78..67a0d48f1b 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -51,8 +51,16 @@ let raw_constr_of_string = e;;
 (* build a term of type constr with type-checking and resolution of 
    implicit syntax *)
 
-let constr_of_string s 
-	= Astterm.interp_constr Evd.empty (Global.env()) (parse_ast s);;
+let constr_of_string s = 
+  Astterm.interp_constr Evd.empty (Global.env()) (parse_ast s);;
+
+(* get the body of a constant *)
+
+open Declarations;;
+
+let constbody_of_string s =
+  let b = Global.lookup_constant (path_of_string s) in
+  Util.out_some b.const_body;;
 
 (* Get the current goal *)
 
@@ -66,3 +74,4 @@ let pf_e gl s =
 
 open Toplevel
 let go = loop
+
-- 
cgit v1.2.3