From 4e68924f48d3f6d5ffdf1cd394b590b5a6e15ea1 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 2 Nov 2009 19:18:23 +0000
Subject: Reverted an incorrect code simplification in function status_changed
 (rewrote it differently to avoid being trapped again).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12460 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/evarutil.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 100bf347f8..2c6d1c0b85 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1109,10 +1109,8 @@ let solve_pattern_eqn env l1 c =
  *)
 
 let status_changed lev (pbty,_,t1,t2) =
-  try ExistentialSet.mem (head_evar t1) lev
-  with NoHeadEvar ->
-  try ExistentialSet.mem (head_evar t2) lev
-  with NoHeadEvar -> false
+  (try ExistentialSet.mem (head_evar t1) lev with NoHeadEvar -> false) or
+  (try ExistentialSet.mem (head_evar t2) lev with NoHeadEvar -> false)
 
 (* Solve pbs (?i x1..xn) = (?i y1..yn) which arises often in fixpoint
  * definitions. We try to unify the xi with the yi pairwise. The pairs
-- 
cgit v1.2.3