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 +++++++++++--
 dev/include         |  1 +
 dev/top_printers.ml |  2 ++
 3 files changed, 14 insertions(+), 2 deletions(-)

(limited to 'dev')

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
+
diff --git a/dev/include b/dev/include
index 0603fed6f2..2a841e4583 100644
--- a/dev/include
+++ b/dev/include
@@ -24,3 +24,4 @@
 #install_printer  (* readable_constraints *)  prevc;;
 #install_printer  (* walking_constraints *)  prwc;;
 #install_printer  (* clenv *) prclenv;;
+#install_printer  (* env *) ppenv;;
\ No newline at end of file
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index e2a91022fa..48b12aa2ed 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -80,6 +80,8 @@ let print_uni u = (pP (pr_uni u))
 
 let pp_universes u = pP [< 'sTR"[" ; pr_universes u ; 'sTR"]" >]
 
+let ppenv e = pP (pr_rel_context e (rel_context e))
+
 let cnt = ref 0
 
 let constr_display csr =
-- 
cgit v1.2.3