new options activated

[helm.git] / helm / software / helena / src / basic_ag / bagReduction.ml

diff --git a/helm/software/helena/src/basic_ag/bagReduction.ml b/helm/software/helena/src/basic_ag/bagReduction.ml
index 287978f5064dcf1a71856d4ab0d52c6798fa546d..cc3cb36f8266b8edb35cf92617f61aae552c90b6 100644 (file)
--- a/helm/software/helena/src/basic_ag/bagReduction.ml
+++ b/helm/software/helena/src/basic_ag/bagReduction.ml
@@ -81,19 +81,19 @@ let push msg f c m a l w =
 let rec whd f c m x = 
 (*   L.warn "entering R.whd"; *)
    match x with
-   | Z.Sort h                    -> f m (Sort_ h)
-   | Z.GRef uri                  ->
+   | Z.Sort h                   -> f m (Sort_ h)
+   | Z.GRef uri                 ->
       let f entry = f m (GRef_ entry) in
       ZE.get_entity f uri
-   | Z.LRef i                    ->
+   | Z.LRef i                   ->
       let f = function
          | Z.Void   -> f m (LRef_ (i, None))
         | Z.Abst t -> f m (LRef_ (i, Some t))
         | Z.Abbr t -> whd f c m t
       in
       get f c m i
-   | Z.Cast (_, t)               -> whd f c m t
-   | Z.Appl (v, t)               -> whd f c {m with s = v :: m.s} t   
+   | Z.Cast (_, t)              -> whd f c m t
+   | Z.Appl (v, t)              -> whd f c {m with s = v :: m.s} t   
    | Z.Bind (a, l, Z.Abst w, t) ->
       begin match m.s with
          | []      -> f m (Bind_ (a, l, w, t))
@@ -102,7 +102,7 @@ let rec whd f c m x =
            let f mc = ZS.subst (whd f c {m with c = mc; s = tl}) nl l t in
            Z.push "!" f m.c a nl (Z.Abbr (Z.Cast (w, v)))
       end
-   | Z.Bind (a, l, b, t)         -> 
+   | Z.Bind (a, l, b, t)        -> 
       let nl = P.new_mark () in
       let f mc = ZS.subst (whd f c {m with c = mc}) nl l t in
       Z.push "!" f m.c a nl b
@@ -124,7 +124,7 @@ let rec ho_whd f c m x =
    whd aux c m x
    
 let ho_whd f st c t =
-   if !G.trace >= level then log1 st "Now scanning" c t;
+   if !G.ct >= level then log1 st "Now scanning" c t;
    ho_whd f c empty_machine t
 
 let rec are_convertible f st a c m1 t1 m2 t2 =
@@ -132,7 +132,7 @@ let rec are_convertible f st a c m1 t1 m2 t2 =
    let rec aux m1 r1 m2 r2 =
 (*   L.warn "entering R.are_convertible_aux"; *)
    let u, t = term_of_whdr r1, term_of_whdr r2 in
-   if !G.trace >= level then log2 st "Now really converting" c u c t;   
+   if !G.ct >= level then log2 st "Now really converting" c u c t;   
    match r1, r2 with
       | Sort_ h1, Sort_ h2                                 ->
          if h1 = h2 then f a else f false 
@@ -189,5 +189,5 @@ and are_convertible_stacks f st a c m1 m2 =
       C.list_fold_left2 f map a m1.s m2.s
 
 let are_convertible f st c u t = 
-   if !G.trace >= level then log2 st "Now converting" c u c t;
+   if !G.ct >= level then log2 st "Now converting" c u c t;
    are_convertible f st true c empty_machine u empty_machine t