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=4b8099fed004c7e92ab152f190b5ca5599fde050;hpb=cf5d6fab96c47ccb7d623d72742717d9b08bae7b;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
index 4b8099fed..f53471414 100644
--- 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";
      (*