1) removed many debug prints

[helm.git] / matitaB / components / ng_tactics / nTacStatus.ml

diff --git a/matitaB/components/ng_tactics/nTacStatus.ml b/matitaB/components/ng_tactics/nTacStatus.ml
index dc534b43058c04a69125cd6fdf87e4d5630512e2..3a07acc05a641de942ae1c88a2e507234d1a8384 100644 (file)
--- a/matitaB/components/ng_tactics/nTacStatus.ml
+++ b/matitaB/components/ng_tactics/nTacStatus.ml
@@ -72,10 +72,10 @@ class type g_pstatus =
   method obj: NCic.obj
  end
 
-class virtual pstatus =
+class virtual pstatus uid =
  fun (o: NCic.obj) ->
  object (self)
-   inherit GrafiteDisambiguate.status
+   inherit GrafiteDisambiguate.status uid
    inherit auto_status
    inherit eq_status
    val obj = o
@@ -189,7 +189,7 @@ let disambiguate status context t ty =
        let status, (_,x) = relocate status context ty in status, Some x 
  in
  let uri,height,metasenv,subst,obj = status#obj in
- let newast, metasenv, subst, status, t = 
+ let metasenv, subst, status, t = 
    GrafiteDisambiguate.disambiguate_nterm status expty context metasenv subst t 
  in
  let new_pstatus = uri,height,metasenv,subst,obj in
@@ -479,10 +479,10 @@ class type ['stack] g_status =
   method stack: 'stack
  end
 
-class virtual ['stack] status =
+class virtual ['stack] status uid =
  fun (o: NCic.obj) (s: 'stack) ->
  object (self)
-   inherit (pstatus o)
+   inherit (pstatus uid o)
    val stack = s
    method stack = stack
    method set_stack s = {< stack = s >}
@@ -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)
 ;;