From 6412f9910328878785ccb3ad6d87fb5dd276cffe Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 16 Oct 2009 12:39:27 +0000
Subject: [PATCH] removed optimization potentially unsound

---
 helm/software/components/ng_kernel/nCicReduction.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index 717644ac5..8fc58f4c9 100644
--- a/helm/software/components/ng_kernel/nCicReduction.ml
+++ b/helm/software/components/ng_kernel/nCicReduction.ml
@@ -269,12 +269,14 @@ let alpha_eq ~test_lambda_source aux test_eq_only metasenv subst context t1 t2 =
        when (Ref.eq r1 r2 && 
          List.length (E.get_relevance r1) >= List.length tl1) ->
      let relevance = E.get_relevance r1 in
+(* if the types were convertible the following optimization is sound
      let relevance = match r1 with
          | Ref.Ref (_,Ref.Con (_,_,lno)) ->
              let _,relevance = HExtlib.split_nth lno relevance in
                HExtlib.mk_list false lno @ relevance
          | _ -> relevance
      in
+*)
      (try
          HExtlib.list_forall_default3_var
           (fun t1 t2 b -> not b || aux true context t1 t2 )
-- 
2.39.2