Locally implemented print_context replaced by CicPp.ppcontext.

diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml
index 3d4fc7126bcc781d041c0f6acf194696cf266b4a..c2407ee73b3625997a21b76cb212296810ef9de7 100644 (file)
--- 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)