X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fbasic_ag%2FbagReduction.ml;fp=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fbasic_ag%2FbagReduction.ml;h=52f04bf0e2406249cdd290bb01bc59138413650d;hb=22fd9c98a22929f0319286c0693fcdaee43a72df;hp=e2e00e39b7f2317f23405367d9dbd7f75ac336a8;hpb=10d33a8c1be31d0c7aeccee8968fd5218ca2510a;p=helm.git

diff --git a/helm/software/lambda-delta/src/basic_ag/bagReduction.ml b/helm/software/lambda-delta/src/basic_ag/bagReduction.ml
index e2e00e39b..52f04bf0e 100644
--- a/helm/software/lambda-delta/src/basic_ag/bagReduction.ml
+++ b/helm/software/lambda-delta/src/basic_ag/bagReduction.ml
@@ -113,14 +113,14 @@ let rec whd f c m x =
 let rec ho_whd f c m x =
 (*   L.warn "entering R.ho_whd"; *)
    let aux m = function
-      | Sort_ h                -> f (Sort h)
-      | Bind_ (_, _, w, _)     -> 
+      | Sort_ h                     -> f (Sort h)
+      | Bind_ (_, _, w, _)          -> 
          let f w = f (Abst w) in unwind_to_term f m w
-      | LRef_ (_, Some w)      -> ho_whd f c m w
-      | GRef_ (_, _, E.Abst w) -> ho_whd f c m w  
-      | GRef_ (_, _, E.Abbr v) -> ho_whd f c m v
-      | LRef_ (_, None)        -> assert false
-      | GRef_ (_, _, E.Void)   -> assert false
+      | LRef_ (_, Some w)           -> ho_whd f c m w
+      | GRef_ (_, _, E.Abst (_, w)) -> ho_whd f c m w  
+      | GRef_ (_, _, E.Abbr v)      -> ho_whd f c m v
+      | LRef_ (_, None)             -> assert false
+      | GRef_ (_, _, E.Void)        -> assert false
    in
    whd aux c m x