From 02ae6637b48f03db431e5722243235710957c5b6 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 5 Feb 2009 10:48:28 +0000 Subject: [PATCH] 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 --- helm/software/components/cic_proof_checking/cicReduction.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml index 311d1880b..6e3436085 100644 --- 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) -> -- 2.39.2