new options activated

[helm.git] / helm / software / helena / src / common / layer.ml

diff --git a/helm/software/helena/src/common/layer.ml b/helm/software/helena/src/common/layer.ml
index ede703d6d787a958ab576c5b89d44470f301d7c4..1ad6cf28cae6b5522bbb37cc33ba6c720d6e1c3c 100644 (file)
--- a/helm/software/helena/src/common/layer.ml
+++ b/helm/software/helena/src/common/layer.ml
@@ -85,18 +85,18 @@ let rec generated st h i =
    let k, n = resolve_key_with_default st default k in 
    if n.s then generated st h i else begin
       if n <> default then KH.replace st k default;
-      if !G.trace >= level then pp_table st; default
+      if !G.ct >= level then pp_table st; default
    end
 
 let assert_finite st n j =
-   if !G.trace >= level then warn (Printf.sprintf "ASSERT FINITE %u" j);
+   if !G.ct >= level then warn (Printf.sprintf "ASSERT FINITE %u" j);
    let rec aux (k, n) j = match n.v with    
       | Fin i when i = j -> true
       | Fin i            ->
          Printf.printf "binder %s is %u but must be %u\n" (P.string_of_mark k) i j; true (**)
       | Inf              ->
          Printf.printf "binder %s is infinite but must be %u\n" (P.string_of_mark k) j; true (**)
-      | Unk              -> n.v <- Fin j; if !G.trace >= level then pp_table st; true
+      | Unk              -> n.v <- Fin j; if !G.ct >= level then pp_table st; true
       | Ref (k, i)       -> n.v <- Fin j; aux (resolve_key st k) (i+j) 
    in
    let k, n = resolve_layer st n in
@@ -106,12 +106,12 @@ let assert_finite st n j =
       aux (k, n) j
 
 let assert_infinite st n =
-   if !G.trace >= level then warn "ASSERT INFINITE";
+   if !G.ct >= level then warn "ASSERT INFINITE";
    let rec aux (k, n) = match n.v with
       | Inf        -> true
       | Fin i      -> 
          Printf.printf "binder %s is %u but must be infinite\n" (P.string_of_mark k) i; true (**)
-      | Unk        -> n.v <- Inf; if !G.trace >= level then pp_table st; true
+      | Unk        -> n.v <- Inf; if !G.ct >= level then pp_table st; true
       | Ref (k, _) -> n.v <- Inf; aux (resolve_key st k) 
    in
    aux (resolve_layer st n)
@@ -132,19 +132,19 @@ let one = finite 1
 let two = finite 2
 
 let rec unknown st =
-   if !G.trace >= level then warn "UNKNOWN";
+   if !G.ct >= level then warn "UNKNOWN";
    let default = empty () in
    let k = P.new_mark () in
    let k, n = resolve_key_with_default st default k in
    if n.s then match n.v with
       | Inf
       | Fin _ -> n
-      | Unk   -> if !G.trace >= level then pp_table st; cell true (Ref (k, 0))
+      | Unk   -> if !G.ct >= level then pp_table st; cell true (Ref (k, 0))
       | Ref _ -> assert false
    else unknown st
  
 let minus st n j =
-   if !G.trace >= level then warn (Printf.sprintf "MINUS %u" j);
+   if !G.ct >= level then warn (Printf.sprintf "MINUS %u" j);
    let rec aux k n j = match n.v with
       | Inf              -> cell false n.v
       | Fin i when i > j -> cell false (Fin (i - j))
@@ -163,14 +163,14 @@ let to_string st n =
    string_of_value k n.v
 
 let assert_not_zero st n =
-   if !G.trace >= level then warn "ASSERT NOT ZERO";
+   if !G.ct >= level then warn "ASSERT NOT ZERO";
    let k, n = resolve_layer st n in
    match n.b, n.v with
       | true, _                -> n.b
 (*      | _   , Fin i when i = 0 ->   
          Printf.printf "^Pi reduction on binder %s\n" (P.string_of_mark k); false *) (**)
 (*      if n.s && n.v = Fin 1 then Printf.printf "Pi reduction on binder %s\n" (P.string_of_mark k); *)      
-      | _                      -> n.b <- true; if !G.trace >= level then pp_table st; n.b
+      | _                      -> n.b <- true; if !G.ct >= level then pp_table st; n.b
 
 let assert_zero st n = assert_finite st n 0
 
@@ -186,9 +186,9 @@ let assert_equal st n1 n2 =
          | Ref _ -> assert false
       else false
    in begin
-   if !G.trace >= level then warn "ASSERT EQUAL";
+   if !G.ct >= level then warn "ASSERT EQUAL";
    if b && k1 <> P.null_mark && k2 <> P.null_mark then begin
-      n1.v <- Ref (k2, 0); if !G.trace >= level then pp_table st
+      n1.v <- Ref (k2, 0); if !G.ct >= level then pp_table st
    end; b end
 
 let is_not_zero st n  =