bumped changelog line to match upload date

[helm.git] / helm / ocaml / cic_proof_checking / cicReductionMachine.ml

diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
index f5684a9510196194727e7a9e48bc9aaf2954146d..f53471414b660a53e7e4c04310c1c0b0383ef54d 100644 (file)
--- 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";
      (*