From e2a81df304c198cc2bdd5d1ffa703ed7eaca9d12 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 23 Jul 2017 04:08:30 +0200
Subject: Remove a few useless evar-normalizations in printing code.

---
 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 3516788022..60a391d49f 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -727,7 +727,7 @@ let default_pr_subgoals ?(pr_first=true)
   match goals with
   | [] ->
       begin
-	let exl = Evarutil.non_instantiated sigma in
+	let exl = Evd.undefined_map sigma in
 	if Evar.Map.is_empty exl then
 	  (str"No more subgoals." ++ print_dependent_evars None sigma seeds)
 	else
-- 
cgit v1.2.3