a non necessary but morally required change. The matched term in

are_convertible is compared with test_eq_only=true (not really needed since
if it reduces to something it is a constructor an thus an application that already honors the test_eq_only=true check for arguments

diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml
index 311d1880b149a4f9afcfd481e8fd4d123e237a54..6e34360850caf0f2f5f48f85cee3c65e060833c7 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicReduction.ml
+++ b/helm/software/components/cic_proof_checking/cicReduction.ml
@@ -980,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) ->