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 4b8099fed004c7e92ab152f190b5ca5599fde050..f53471414b660a53e7e4c04310c1c0b0383ef54d 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
@@ -544,7 +544,7 @@ if List.mem uri params then prerr_endline "---- OK2" ;
           )
      | (k, e, ens, (C.Meta (n,l) as t), s) ->
         (try 
-          let (_, term) = CicUtil.lookup_subst n subst in
+          let (_, term,_) = CicUtil.lookup_subst n subst in
            reduce (k, e, ens,CicSubstitution.lift_meta l term,s)
         with  CicUtil.Subst_not_found _ ->
            let t' = unwind k e ens t in
@@ -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";
      (*