X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_tactics%2FnTacStatus.ml;h=26e4ade40b2c92d3dfb986c9529c6d9c91b95c9e;hb=db020b4218272e2e35641ce3bc3b0a9b3afda899;hp=3684c051f5913ea8adc9c4eca53272a2113b9b2e;hpb=6c702f5054d7975f76911ba62da9bfa33d3ed0fa;p=helm.git diff --git a/matitaB/components/ng_tactics/nTacStatus.ml b/matitaB/components/ng_tactics/nTacStatus.ml index 3684c051f..26e4ade40 100644 --- a/matitaB/components/ng_tactics/nTacStatus.ml +++ b/matitaB/components/ng_tactics/nTacStatus.ml @@ -27,7 +27,7 @@ module NRef = NReference let wrap fname f x = try f x with - | MultiPassDisambiguator.DisambiguationError _ + | GrafiteDisambiguate.Error _ | NCicRefiner.RefineFailure _ | NCicUnification.UnificationFailure _ | NCicTypeChecker.TypeCheckerFailure _ @@ -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) ;;