From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 16 Jun 2005 16:40:55 +0000 (+0000)
Subject: Locally implemented print_context replaced by CicPp.ppcontext.
X-Git-Tag: INDEXING_NO_PROOFS~128
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=aaab725d107d2306a2944826b38512c2a4b1c182;p=helm.git

Locally implemented print_context replaced by CicPp.ppcontext.
---

diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml
index 3d4fc7126..c2407ee73 100644
--- a/helm/ocaml/tactics/autoTactic.ml
+++ b/helm/ocaml/tactics/autoTactic.ml
@@ -27,30 +27,6 @@
 
 (* let debug_print = fun _ -> () *)
 
-(* Da rimuovere, solo per debug*)
-let print_context ctx =
-    let print_name =
-     function
-        Cic.Name n -> n
-      | Cic.Anonymous -> "_"
-    in
-     List.fold_right
-      (fun i (output,context) ->
-        let (newoutput,context') =
-         match i with
-            Some (n,Cic.Decl t) ->
-              print_name n ^ ":" ^ CicPp.pp t context ^ "\n", (Some n)::context
-          | Some (n,Cic.Def (t,None)) ->
-              print_name n ^ ":=" ^ CicPp.pp t context ^ "\n", (Some n)::context
-          | None ->
-              "_ ?= _\n", None::context
-          | Some (_,Cic.Def (_,Some _)) -> assert false
-        in
-         output^newoutput,context'
-      ) ctx ("",[])
-  ;;
-
-
 let search_theorems_in_context status =
   let (proof, goal) = status in
   let module C = Cic in
@@ -110,9 +86,9 @@ let rec auto dbd = function
 	  Some (ey, ty) ->
             (* the goal is still there *)
             (*
-	    debug_print ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
-	    debug_print ("CURRENT PROOF = " ^ (CicPp.ppterm p));
-	    debug_print ("CURRENT HYP = " ^ (fst (print_context ey)));
+	    debug_print ("CURRENT GOAL = " ^ CicPp.ppterm ty);
+	    debug_print ("CURRENT PROOF = " ^ CicPp.ppterm p);
+	    debug_print ("CURRENT HYP = " ^ CicPp.ppcontext ey);
             *)
             (* if the goal contains metavariables we use the input
                signature for at_most constraints *)
@@ -300,9 +276,9 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
 	    [] (* the empty list means no choices, i.e. failure *)
 	| No _ 
 	| NotYetInspected ->
-	      debug_print ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
-	      debug_print ("CURRENT PROOF = " ^ (CicPp.ppterm p));
-	      debug_print ("CURRENT HYP = " ^ (fst (print_context ey)));
+	      debug_print ("CURRENT GOAL = " ^ CicPp.ppterm ty);
+	      debug_print ("CURRENT PROOF = " ^ CicPp.ppterm p);
+	      debug_print ("CURRENT HYP = " ^ CicPp.ppcontext ey);
 	    let sign, new_sign =
 	      if is_meta_closed then
 		None, Some (MetadataConstraints.signature_of ty)