- initial support for abstractions with explicit levels

[helm.git] / helm / software / lambda-delta / src / basic_ag / bagReduction.ml

diff --git a/helm/software/lambda-delta/src/basic_ag/bagReduction.ml b/helm/software/lambda-delta/src/basic_ag/bagReduction.ml
index e2e00e39b7f2317f23405367d9dbd7f75ac336a8..52f04bf0e2406249cdd290bb01bc59138413650d 100644 (file)
--- 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