From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 30 Mar 2006 11:12:53 +0000 (+0000)
Subject: Bug fixed: terms with a Cast used to raise assert false when whd was avoided
X-Git-Tag: 0.4.95@7852~1543
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=afc19735fc5b88c8e841d6e62e58f21a81f06d8c;p=helm.git

Bug fixed: terms with a Cast used to raise assert false when whd was avoided
by the conversion strategy.
---

diff --git a/components/cic_proof_checking/cicReduction.ml b/components/cic_proof_checking/cicReduction.ml
index bd8d07b8d..de3bf61f4 100644
--- a/components/cic_proof_checking/cicReduction.ml
+++ b/components/cic_proof_checking/cicReduction.ml
@@ -792,7 +792,7 @@ let (===) x y =
 let are_convertible whd ?(subst=[]) ?(metasenv=[])  =
  let heuristic = ref true in
  let rec aux test_equality_only context t1 t2 ugraph =
-  let aux2 test_equality_only t1 t2 ugraph =
+  let rec aux2 test_equality_only t1 t2 ugraph =
 
    (* this trivial euristic cuts down the total time of about five times ;-) *)
    (* this because most of the time t1 and t2 are "sintactically" the same   *)
@@ -1008,7 +1008,8 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1);
              fl1 fl2 (true,ugraph)
             else
               false,ugraph
-        | (C.Cast _, _) | (_, C.Cast _)
+        | C.Cast (bo,_),t -> aux2 test_equality_only bo t ugraph
+        | t,C.Cast (bo,_) -> aux2 test_equality_only t bo ugraph
         | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
         | (_,_) -> false,ugraph
     end