]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/basic_rg/brgReduction.ml
new syntax of abstractions propagated to complete_rg
[helm.git] / helm / software / helena / src / basic_rg / brgReduction.ml
index 774b016a19969dad5d5905c36e9000598dcd68db..bb31fc9768a77d98c7e8150b4003206d58c1774b 100644 (file)
@@ -93,7 +93,7 @@ let get m i =
 (* to share *)
 let rec step st m r = 
    if !G.trace >= sublevel then 
-   log1 st (Printf.sprintf "entering R.step: l:%u n:%s" m.l (match m.n with Some n -> string_of_int n | None -> "infinite")) m.e r;
+   log1 st (Printf.sprintf "entering R.step: l=%u, n=%s," m.l (match m.n with Some n -> string_of_int n | None -> "infinite")) m.e r;
    match r with
    | B.Sort (a, h)                       ->
       if assert_tstep m false then