+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
+
+open Printf
+
+let debug = false
+let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
+
+open Continuationals.Stack
+open NTacStatus
+module Ast = CicNotationPt
+
+let auto_tac status =
+ prerr_endline "I teoremi noti sono";
+ NDiscriminationTree.DiscriminationTree.iter status#auto_cache
+ (fun _ t ->
+ List.iter (fun t ->
+ prerr_endline
+ (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t))
+ (NDiscriminationTree.TermSet.elements t));
+ status
+;;