From 43a43ea30b30e609ce28c69d50bc276c84073486 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Wed, 15 Jun 2016 17:48:17 +0200
Subject: Prevent a useless evar normalization in Clenvtac.unify.

---
 proofs/clenvtac.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs/clenvtac.ml')

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 08e6c91de..da2eee32a 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -120,7 +120,7 @@ let fail_quick_unif_flags = {
 let unify ?(flags=fail_quick_unif_flags) m =
   Proofview.Goal.enter { enter = begin fun gl ->
     let env = Tacmach.New.pf_env gl in
-    let n = Tacmach.New.pf_nf_concl gl in
+    let n = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in
     let evd = clear_metas (Tacmach.New.project gl) in
     try
       let evd' = w_unify env evd CONV ~flags m n in
-- 
cgit v1.2.3