From d45787d8c1bd22f27b64f214a9fb8f54e69c9533 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 30 Jan 2009 14:51:27 +0000 Subject: [PATCH] fix convertibility in case of application test_eq_only is =true for arguments, since we dont know if reduction eventually moves them in contravariant position --- .../software/components/ng_kernel/nCicReduction.ml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml index 6105dd3a0..8012f0b75 100644 --- a/helm/software/components/ng_kernel/nCicReduction.ml +++ b/helm/software/components/ng_kernel/nCicReduction.ml @@ -257,7 +257,7 @@ let are_convertible ~metasenv ~subst = in (try HExtlib.list_forall_default3_var - (fun t1 t2 b -> not b || aux test_eq_only context t1 t2 ) + (fun t1 t2 b -> not b || aux true context t1 t2 ) tl1 tl2 true relevance with Invalid_argument _ -> false | HExtlib.FailureAt fail -> @@ -272,7 +272,7 @@ let are_convertible ~metasenv ~subst = let _,tl2 = HExtlib.split_nth (fail+1) tl2 in try HExtlib.list_forall_default3 - (fun t1 t2 b -> not b || aux test_eq_only context t1 t2) + (fun t1 t2 b -> not b || aux true context t1 t2) tl1 tl2 true relevance with Invalid_argument _ -> false else false) @@ -282,7 +282,7 @@ let are_convertible ~metasenv ~subst = let relevance = !get_relevance ~metasenv ~subst context hd1 tl1 in (try HExtlib.list_forall_default3 - (fun t1 t2 b -> not b || aux test_eq_only context t1 t2) + (fun t1 t2 b -> not b || aux true context t1 t2) tl1 tl2 true relevance with Invalid_argument _ -> false) @@ -339,7 +339,7 @@ let are_convertible ~metasenv ~subst = R.reduce ~delta ~subst context m1, R.reduce ~delta ~subst context m2 in - let rec convert_machines + let rec convert_machines test_eq_only ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2), norm2 as m2) = (alpha_eq test_eq_only @@ -354,11 +354,11 @@ let are_convertible ~metasenv ~subst = not b || let t1 = RS.from_stack t1 in let t2 = RS.from_stack t2 in - convert_machines (put_in_whd t1 t2)) s1 s2 true relevance + convert_machines true (put_in_whd t1 t2)) s1 s2 true relevance with Invalid_argument _ -> false) || - (not (norm1 && norm2) && convert_machines (small_delta_step m1 m2)) + (not (norm1 && norm2) && convert_machines test_eq_only (small_delta_step m1 m2)) in - convert_machines (put_in_whd (0,[],t1,[]) (0,[],t2,[])) + convert_machines test_eq_only (put_in_whd (0,[],t1,[]) (0,[],t2,[])) in aux false ;; -- 2.39.2