From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 5 Feb 2009 10:48:28 +0000 (+0000)
Subject: a non necessary but morally required change. The matched term in
X-Git-Tag: make_still_working~4210
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=02ae6637b48f03db431e5722243235710957c5b6;p=helm.git

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 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) ->