From fbf196647d0abd1dbbeda690e2065426d33e5156 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Tue, 10 Jul 2012 10:08:04 +0000
Subject: Another correction to the dependent existential variable printing for
 emacs mode.

Hopefully fixes Bug 2678 this time. Much saner and more compact code.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15573 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 printing/printer.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index 0386fc6522..23e6e277fb 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -334,7 +334,7 @@ let default_pr_subgoal n sigma =
 
 let emacs_print_dependent_evars sigma seeds =
   let evars () =
-    let evars = Evarutil.evars_of_evars_in_types_of_list sigma seeds in
+    let evars = Evarutil.gather_dependent_evars sigma seeds in
     let evars =
       Intmap.fold begin fun e i s ->
 	let e' = str (string_of_existential e) in
-- 
cgit v1.2.3