From e3be8cdf7c4aa3882028d460267b136dcc36754a Mon Sep 17 00:00:00 2001
From: filliatr
Date: Tue, 14 Dec 1999 08:03:32 +0000
Subject: pretty-printers pour le debugger

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

(limited to 'dev/base_include')

diff --git a/dev/base_include b/dev/base_include
index 8964873eb0..f314b35582 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -47,14 +47,17 @@ let raw_constr_of_string s =
     (parse_ast s);;
 
 let e s    = 
-   constr_of_com Evd.empty (Global.env()) (parse_ast s);;
+   Astterm.constr_of_com Evd.empty (Global.env()) (parse_ast s);;
 
 (* Get the current goal *)
 
-let getgoal x = top_goal_of_pftreestate (get_pftreestate x);;
+let getgoal x = top_goal_of_pftreestate (Pfedit.get_pftreestate x);;
 
-let get_nth_goal n = nth_goal_of_pftreestate n (get_pftreestate ());;
+let get_nth_goal n = nth_goal_of_pftreestate n (Pfedit.get_pftreestate ());;
 let current_goal () = get_nth_goal 1;;
 
 let pf_e gl s = 
-    constr_of_com (project gl) (pf_env gl) (parse_ast s);;
+    Astterm.constr_of_com (project gl) (pf_env gl) (parse_ast s);;
+
+open Toplevel
+let go = loop
-- 
cgit v1.2.3