X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicReductionMachine.ml;h=f53471414b660a53e7e4c04310c1c0b0383ef54d;hb=ac7687ce66526f905874ed99a845223c853c558a;hp=f5684a9510196194727e7a9e48bc9aaf2954146d;hpb=8ca2202b7bf9b11b69562502f6dfb168b7efb0e2;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
index f5684a951..f53471414 100644
--- a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
@@ -769,17 +769,21 @@ module R = Reduction
  ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;;
 *)
 module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;
+module U = UriManager;;
 
 let whd = R.whd;;
 
+  (* mimic ocaml (<< 3.08) "=" behaviour. Tests physical equality first then
+    * fallbacks to structural equality *)
+let (===) x y = (Pervasives.compare x y = 0)
+
 (* t1, t2 must be well-typed *)
 let are_convertible ?(subst=[]) ?(metasenv=[]) =
- let module U = UriManager in
  let rec aux test_equality_only context t1 t2 =
   let aux2 test_equality_only t1 t2 =
    (* 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   *)
-   if t1 = t2 then
+   if t1 === t2 then
     true
    else
     begin
@@ -904,8 +908,10 @@ let are_convertible ?(subst=[]) ?(metasenv=[]) =
         | (_,_) -> false
     end
   in
+(*
    if aux2 test_equality_only t1 t2 then true
    else
+*)
      begin
      debug t1 [t2] "PREWHD";
      (*