From 342fed039e53f00ff8758513149f8d41fa3a2e99 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 3 Jul 2015 21:14:09 +0200
Subject: Evarconv.ml: small cut-elimination, saving useless zip.

---
 pretyping/evarconv.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 4fed09d6f4..3f4411c058 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -417,7 +417,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     let not_only_app = Stack.not_purely_applicative skM in
     let f1 i =
       match Stack.list_of_app_stack skF with
-      | None -> default_fail evd
+      | None -> quick_fail evd
       | Some lF -> 
         let tM = Stack.zip apprM in
 	  miller_pfenning on_left
-- 
cgit v1.2.3