- alpha convertibility test disabled for now (it needs better implementation)

[helm.git] / helm / software / lambda-delta / basic_rg / brgReduction.ml

diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.ml b/helm/software/lambda-delta/basic_rg/brgReduction.ml
index 26663cf5f1ec5350d20138c919837f311fa3ec6a..4b1d287d951fe6a9d4bf12dc468a9acfe948c636 100644 (file)
--- a/helm/software/lambda-delta/basic_rg/brgReduction.ml
+++ b/helm/software/lambda-delta/basic_rg/brgReduction.ml
@@ -84,11 +84,11 @@ let rec step f ?(delta=false) ?(rt=false) m x =
    | B.GRef (a, uri)         ->
       let f = function
          | _, _, B.Abbr v when delta ->
-            P.add ~gdelta:1 ();
-           step f ~delta ~rt m v
-         | _, _, B.Abst w when rt   ->
-            P.add ~grt:1 ();
-           step f ~delta ~rt m w        
+           P.add ~gdelta:1 (); step f ~delta ~rt m v
+         | _, _, B.Abst w when rt    ->
+            P.add ~grt:1 (); step f ~delta ~rt m w      
+        | _, _, B.Void              ->
+           assert false
         | e, _, b                   ->
            f m (Some (e, b)) x
       in
@@ -102,7 +102,7 @@ let rec step f ?(delta=false) ?(rt=false) m x =
             P.add ~lrt:1 ();
             step f ~delta ~rt {m with c = c} w
         | B.Void            ->
-           f {m with c = c} None x
+           assert false
         | b                 ->
            let f e = f {m with c = c} (Some (e, b)) x in 
            B.apix C.err f a
@@ -221,7 +221,7 @@ let assert_conversion f ?(si=false) ?(rt=false) mw u w v =
          if r then begin L.unbox level; f () end else error3 mw.c v w u
       in
       let g r = if r then f r else ac f ~si true mu u mw w in
-      if S.eq mu mw then are_alpha_convertible g u w else g false
+(*      if S.eq mu mw then are_alpha_convertible g u w else *) g false
    in
    if rt then domain f mw u else f mw u