X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicReduction.ml;h=6e34360850caf0f2f5f48f85cee3c65e060833c7;hb=ec07ff398325533d848da92e9dc69852d24b78a5;hp=ff19dff194bf2720b6f2ba6aaadaa74bad6f7efb;hpb=0b15dfdee3357a626c77d30599e87a83ab34e471;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml
index ff19dff19..6e3436085 100644
--- a/helm/software/components/cic_proof_checking/cicReduction.ml
+++ b/helm/software/components/cic_proof_checking/cicReduction.ml
@@ -906,13 +906,18 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1);
            else
              false,ugraph
         | (C.Appl l1, C.Appl l2) ->
+           let b, ugraph = 
+             aux test_equality_only context (List.hd l1) (List.hd l2) ugraph
+           in
+           if not b then false, ugraph
+           else
            (try
              List.fold_right2
                (fun  x y (b,ugraph) -> 
                  if b then
-                   aux test_equality_only context x y ugraph
+                   aux true context x y ugraph
                  else
-                   false,ugraph) l1 l2 (true,ugraph)
+                   false,ugraph) (List.tl l1) (List.tl l2) (true,ugraph)
             with
              Invalid_argument _ -> false,ugraph
            )
@@ -975,7 +980,7 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1);
              let b'',ugraph''=aux test_equality_only context 
                  outtype1 outtype2 ugraph in
              if b'' then 
-               let b''',ugraph'''= aux test_equality_only context 
+               let b''',ugraph'''= aux true context 
                    term1 term2 ugraph'' in
                List.fold_right2
                  (fun x y (b,ugraph) -> 
@@ -1060,7 +1065,7 @@ prerr_endline ("PREWHD: " ^ CicPp.ppterm t1 ^ " <===> " ^ CicPp.ppterm t2);
    let t2' = whd ?delta:(Some true) ?subst:(Some subst) context t2 in
     debug t1' [t2'] "POSTWHD";
 *)
-let rec convert_machines ugraph =
+let rec convert_machines test_equality_only ugraph =
  function
     [] -> true,ugraph
   | ((k1,env1,ens1,h1,s1),(k2,env2,ens2,h2,s2))::tl ->
@@ -1085,11 +1090,11 @@ let rec convert_machines ugraph =
        in
         match problems with
            None -> false,ugraph
-         | Some problems -> convert_machines ugraph problems
+         | Some problems -> convert_machines true ugraph problems
       else
        res
 in
- convert_machines ugraph
+ convert_machines test_equality_only ugraph
   [R.reduce ~delta:true ~subst context (0,[],[],t1,[]),
    R.reduce ~delta:true ~subst context (0,[],[],t2,[])]
 (*prerr_endline ("POSTWH: " ^ CicPp.ppterm t1' ^ " <===> " ^ CicPp.ppterm t2');*)