From dcaefd4a668617504aaf335ed346598b03a80ba1 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 11 Jan 2006 09:47:32 +0000
Subject: Restructuration et simplification des fonctions d'affichage, de
 détypage et d'"externalisation"; standardisation du nom des fonctions
 d'affichage

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7837 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ide/coq.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'ide')

diff --git a/ide/coq.ml b/ide/coq.ml
index 0e208028c4..a45a56dc40 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -249,7 +249,7 @@ type goal = hyp list * concl
 let prepare_hyp sigma env ((i,c,d) as a) =
   env, sigma,
   ((i,string_of_id i),c,d), 
-  (msg (pr_var_decl env a), msg (prterm_env_at_top env d))
+  (msg (pr_var_decl env a), msg (pr_lconstr_env_at_top env d))
 
 let prepare_hyps sigma env =
   assert (rel_context env = []);
@@ -263,7 +263,7 @@ let prepare_hyps sigma env =
 let prepare_goal sigma g =
   let env = evar_env g in
   (prepare_hyps sigma env,
-   (env, sigma, g.evar_concl, msg (prterm_env_at_top env g.evar_concl)))
+   (env, sigma, g.evar_concl, msg (pr_lconstr_env_at_top env g.evar_concl)))
 
 let get_current_goals () = 
     let pfts = get_pftreestate () in
-- 
cgit v1.2.3