diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-05-07 16:23:49 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-05-07 16:23:49 +0000 |
| commit | fd9a61f49d7fd5613e0ff39b600fe973b4c7c9c9 (patch) | |
| tree | 593623b7f6484ab135c5f8b1c502e315be56cd56 | |
| parent | 770bc83b03d1be4e87a56d0ed06adeb8ad4ba067 (diff) | |
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
| -rw-r--r-- | ide/coq.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index 274d9e46b..2338a8747 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 |