application arguments are compared with test_eq_only=true

diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml
index ff19dff194bf2720b6f2ba6aaadaa74bad6f7efb..311d1880b149a4f9afcfd481e8fd4d123e237a54 100644 (file)
--- 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
            )
@@ -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');*)