From a9df5940e0b362f627abf500e056e197e403c8e1 Mon Sep 17 00:00:00 2001
From: barras
Date: Wed, 3 May 2006 12:02:44 +0000
Subject: bug #1096: whd_stack on one arg of conversion had side-effect on the
 other arg

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8782 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/reduction.ml | 16 ++++++++++++----
 1 file changed, 12 insertions(+), 4 deletions(-)

(limited to 'kernel/reduction.ml')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 2467e941fb..4aa7c57539 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -291,10 +291,18 @@ and eqappr cv_pb infos appr1 appr2 cuniv =
            convert_stacks infos lft1 lft2 v1 v2 u2
          else raise NotConvertible
 
-    | ( (FLetIn _, _) | (_, FLetIn _) | (FCases _,_) | (_,FCases _)
-      | (FApp _,_) | (_,FApp _) | (FCLOS _, _) | (_,FCLOS _)
-      | (FLIFT _, _) | (_,FLIFT _) | (FLOCKED,_) | (_,FLOCKED)) ->
-        anomaly "Unexpected term returned by fhnf"
+    (* Can happen because whd_stack on one arg may have side-effects
+       on the other arg and coulb be no more in hnf... *)
+    | ( (FLetIn _, _) | (FCases _,_) | (FApp _,_)
+      | (FCLOS _, _) | (FLIFT _, _)) ->
+        eqappr cv_pb infos (lft1, whd_stack infos hd1 v1) appr2 cuniv
+
+    | ( (_, FLetIn _) | (_,FCases _) | (_,FApp _)
+      | (_,FCLOS _) | (_,FLIFT _)) ->
+        eqappr cv_pb infos (lft1, whd_stack infos hd1 v1) appr2 cuniv
+
+    (* Should not happen because whd_stack unlocks references *)
+    | ((FLOCKED,_) | (_,FLOCKED)) -> assert false
 
      | _ -> raise NotConvertible
 
-- 
cgit v1.2.3