X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fbasic_ag%2FbagReduction.ml;h=e26a7ec1ed29eec594186fbae3013d1f988f5a72;hp=323de4c9f9c665fbd2488d5fde1133f7937a30f1;hb=88977b2d546e547e23b046792fe2ad8f6ff192a4;hpb=fdb80b08af83b86759833142456ce3c4f84cd80e

diff --git a/helm/software/helena/src/basic_ag/bagReduction.ml b/helm/software/helena/src/basic_ag/bagReduction.ml
index 323de4c9f..e26a7ec1e 100644
--- a/helm/software/helena/src/basic_ag/bagReduction.ml
+++ b/helm/software/helena/src/basic_ag/bagReduction.ml
@@ -114,14 +114,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
    
@@ -147,8 +147,8 @@ ELSE () END;
       | GRef_ (_, {E.n_apix = a1}, _, E.Abst _), 
         GRef_ (_, {E.n_apix = a2}, _, E.Abst _)       ->
          if a1 = a2 then are_convertible_stacks f st a c m1 m2 else f false
-      | GRef_ (_, {E.n_apix = a1}, _, E.Abbr v1), 
-        GRef_ (_, {E.n_apix = a2}, _, E.Abbr v2)      ->
+      | GRef_ (_, {E.n_apix = a1}, _, E.Abbr (_, v1)), 
+        GRef_ (_, {E.n_apix = a2}, _, E.Abbr (_, v2)) ->
          if a1 = a2 then
 	    let f a = 
 	       if a then f a else are_convertible f st true c m1 v1 m2 v2
@@ -157,9 +157,9 @@ ELSE () END;
 	 else
 	 if a1 < a2 then whd (aux m1 r1) c m2 v2 else
 	 whd (aux_rev m2 r2) c m1 v1
-      | _, GRef_ (_, _, _, E.Abbr v2)                 ->
+      | _, GRef_ (_, _, _, E.Abbr (_, v2))            ->
          whd (aux m1 r1) c m2 v2
-      | GRef_ (_, _, _, E.Abbr v1), _                 ->
+      | GRef_ (_, _, _, E.Abbr (_, v1)), _            ->
 	 whd (aux_rev m2 r2) c m1 v1      
       | Bind_ (y1, l1, w1, t1), Bind_ (_, l2, w2, t2) ->
 	   let l = P.new_mark () in