From cf906af70f5c48cab99bd89047af0b2831850cf1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sun, 23 Jul 2017 03:40:16 +0200
Subject: Printing goals does not evar-normalizes beforehand anymore.

---
 printing/printer.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index 0d8168be9..e9d104b49 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -479,7 +479,8 @@ let pr_transparent_state (ids, csts) =
 
 (* display complete goal *)
 let default_pr_goal gs =
-  let (g,sigma) = Goal.V82.nf_evar (project gs) (sig_it gs) in
+  let g = sig_it gs in
+  let sigma = project gs in
   let env = Goal.V82.env sigma g in
   let concl = Goal.V82.concl sigma g in
   let goal =
-- 
cgit v1.2.3