From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 23 Aug 2009 15:15:26 +0000 (+0000)
Subject: - alpha convertibility test disabled for now (it needs better implementation)
X-Git-Tag: make_still_working~3524
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=58087f01e01502c1544c4186507089a1013b5153;p=helm.git

- alpha convertibility test disabled for now (it needs better implementation)
- some icons related to lambda-delta are now available
---

diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.ml b/helm/software/lambda-delta/basic_rg/brgReduction.ml
index 26663cf5f..4b1d287d9 100644
--- 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
 
diff --git a/helm/software/lambda-delta/icons/basic-32.png b/helm/software/lambda-delta/icons/basic-32.png
new file mode 100644
index 000000000..350f6bcb0
Binary files /dev/null and b/helm/software/lambda-delta/icons/basic-32.png differ
diff --git a/helm/software/lambda-delta/icons/crux-32.png b/helm/software/lambda-delta/icons/crux-32.png
new file mode 100644
index 000000000..fe369d292
Binary files /dev/null and b/helm/software/lambda-delta/icons/crux-32.png differ
diff --git a/helm/software/lambda-delta/icons/helena-32.png b/helm/software/lambda-delta/icons/helena-32.png
new file mode 100644
index 000000000..4a065aefe
Binary files /dev/null and b/helm/software/lambda-delta/icons/helena-32.png differ