From f5a8095075c8677efe5ee89b1d7ec53b1b10082b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 19 Oct 2006 07:46:03 +0000
Subject: coqide: affichage des sous-buts et hypothèses et métas comme types de
 telle sorte que les coercions vers sortclass ne soient pas affichées (comme
 dans coqtop)

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

diff --git a/ide/coq.ml b/ide/coq.ml
index 3d489dcb54..4afb677d5c 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -261,7 +261,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 (pr_lconstr_env_at_top env d))
+  (msg (pr_var_decl env a), msg (pr_ltype_env env d))
 
 let prepare_hyps sigma env =
   assert (rel_context env = []);
@@ -275,7 +275,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 (pr_lconstr_env_at_top env g.evar_concl)))
+   (env, sigma, g.evar_concl, msg (pr_ltype_env_at_top env g.evar_concl)))
 
 let prepare_hyps_filter info sigma env =
   assert (rel_context env = []);
@@ -291,7 +291,7 @@ let prepare_hyps_filter info sigma env =
 
 let prepare_meta sigma env (m,typ)  =
   env, sigma, 
-  (msg (str " ?" ++ int m ++ str " : " ++ pr_lconstr_env_at_top env typ))
+  (msg (str " ?" ++ int m ++ str " : " ++ pr_ltype_env_at_top env typ))
 
 let prepare_metas info sigma env =
   List.fold_right 
diff --git a/parsing/printer.mli b/parsing/printer.mli
index c63d7d71f0..dd2a7bad06 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -35,6 +35,7 @@ val pr_lconstr             : constr -> std_ppcmds
 val pr_constr_env          : env -> constr -> std_ppcmds
 val pr_constr              : constr -> std_ppcmds
 
+val pr_ltype_env_at_top    : env -> types -> std_ppcmds
 val pr_ltype_env           : env -> types -> std_ppcmds
 val pr_ltype               : types -> std_ppcmds
 
-- 
cgit v1.2.3