]> matita.cs.unibo.it Git - helm.git/blobdiff - matitaB/components/ng_tactics/nTacStatus.ml
1) removed many debug prints
[helm.git] / matitaB / components / ng_tactics / nTacStatus.ml
index 3684c051f5913ea8adc9c4eca53272a2113b9b2e..3a07acc05a641de942ae1c88a2e507234d1a8384 100644 (file)
@@ -500,6 +500,8 @@ type 'status tactic = #tac_status as 'status -> 'status
 
 let pp_tac_status (status: #tac_status) = 
   prerr_endline (status#ppobj status#obj);
+  (* let a,p = NCicParamod.size_of_state status#eq_cache in
+  prerr_endline ("number of actives: " ^ string_of_int a ^ "and number of passives: " ^ string_of_int p) *)
   prerr_endline ("STACK:\n" ^ Continuationals.Stack.pp status#stack)
 ;;