From bb43103f7ecea16e634d448215f24d6d55d56eb1 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 13 Jun 2016 16:37:29 +0200
Subject: evar_conv: Refine occur_rigidly

This avoids postponing constraints which will surely produce
an occur-check and allow to backtrack on first-order unifications
producing those constraints directly (e.g. to apply eta).
(fixes HoTT/HoTT with 8.5).
---
 pretyping/evarconv.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 96c90e2fc0..aead1cb35f 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -97,8 +97,7 @@ let position_problem l2r = function
   | CUMUL -> Some l2r
 
 let occur_rigidly ev evd t = 
-  let (l, app) = decompose_app_vect t in 
-  let rec aux t = 
+  let rec aux t =
     match kind_of_term (whd_evar evd t) with
     | App (f, c) -> if aux f then Array.exists aux c else false
     | Construct _ | Ind _ | Sort _ | Meta _ | Fix _ | CoFix _ -> true
@@ -110,7 +109,7 @@ let occur_rigidly ev evd t =
     | Prod (_, b, t) -> ignore(aux b || aux t); true
     | Rel _ | Var _ -> false
     | Case _ -> false
-  in Array.exists (fun t -> try ignore(aux t); false with Occur -> true) app
+  in try ignore(aux t); false with Occur -> true
 
 (* [check_conv_record env sigma (t1,stack1) (t2,stack2)] tries to decompose 
    the problem (t1 stack1) = (t2 stack2) into a problem
-- 
cgit v1.2.3