From b00cb9ccbb02e2aa913294887749fff79b0adad5 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 10 Mar 2008 10:22:45 +0000
Subject: Une passe sur l'unification des evars (suite aux commits 10124,
 10125, 10145) - Correction bug des filtres dans define_evar_as_abstraction -
 Nettoyage, documentation et réorganisations diverses

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

(limited to 'parsing/printer.ml')

diff --git a/parsing/printer.ml b/parsing/printer.ml
index 218ba4150c..3e13e13927 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -253,7 +253,7 @@ let pr_subgoal_metas metas env=
 
 (* display complete goal *)
 let default_pr_goal g =
-  let env = evar_env g in
+  let env = evar_unfiltered_env g in
   let preamb,thesis,penv,pc =
     if g.evar_extra = None then
           mt (), mt (),
@@ -278,12 +278,17 @@ let pr_concl n g =
     str (emacs_str (String.make 1 (Char.chr 253)) "")  ++
       str "subgoal " ++ int n ++ str " is:" ++ cut () ++ str" "  ++ pc
 
-
 (* display evar type: a context and a type *)
 let pr_evgl_sign gl = 
-  let ps = pr_named_context_of (evar_env gl) in
+  let ps = pr_named_context_of (evar_unfiltered_env gl) in
+  let _,l = list_filter2 (fun b c -> not b) (evar_filter gl,evar_context gl) in
+  let ids = List.rev (List.map pi1 l) in
+  let warn =
+    if ids = [] then mt () else
+      (str "(" ++ prlist_with_sep pr_coma pr_id ids ++ str " cannot be used)")
+  in
   let pc = pr_lconstr gl.evar_concl in
-  hov 0 (str"["  ++ ps ++ spc () ++ str"|- "  ++ pc ++ str"]")
+  hov 0 (str"[" ++ ps ++ spc () ++ str"|- "  ++ pc ++ str"]" ++ spc () ++ warn)
 
 (* Print an enumerated list of existential variables *)
 let rec pr_evars_int i = function
-- 
cgit v1.2.3