From aaab725d107d2306a2944826b38512c2a4b1c182 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 16 Jun 2005 16:40:55 +0000 Subject: [PATCH] Locally implemented print_context replaced by CicPp.ppcontext. --- helm/ocaml/tactics/autoTactic.ml | 36 ++++++-------------------------- 1 file changed, 6 insertions(+), 30 deletions(-) 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) -- 2.39.2