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

1 files changed, 11 insertions, 2 deletions

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
+