From fd9a61f49d7fd5613e0ff39b600fe973b4c7c9c9 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Fri, 7 May 2010 16:23:49 +0000
Subject: Fix bug #2315 : printing of defined evars in Coqide.

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

diff --git a/ide/coq.ml b/ide/coq.ml
index 274d9e46b0..2338a87476 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -548,8 +548,10 @@ let goals coqtop =
       let process_goal g =
         let env = Goal.V82.env sigma g in
         let ccl =
-          string_of_ppcmds (pr_ltype_env_at_top env (Goal.V82.concl sigma g)) in
+	  let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in
+          string_of_ppcmds (pr_ltype_env_at_top env norm_constr) in
         let process_hyp h_env d acc =
+	  let d = Term.map_named_declaration (Reductionops.nf_evar sigma) d in
           (string_of_ppcmds (pr_var_decl h_env d), hyp_next_tac sigma h_env d)::acc in
         let hyps =
           List.rev (Environ.fold_named_context process_hyp env ~init:[]) in
-- 
cgit v1.2.3