Added a filter for uris in tactic "auto".

[helm.git] / helm / ocaml / tactics / variousTactics.ml

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index bb5be64d8837a8592560ecaf7ef8a3f6072672e1..f8c9cfa94dd409b67f65cbbfe332681473978eef 100644 (file)
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -23,6 +23,34 @@
  * http://cs.unibo.it/helm/.
  *)
 
+ 
+(* 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
@@ -76,6 +104,7 @@ else
   match meta_inf with
       Some (ey, ty) ->
         prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
+        prerr_endline ("CURRENT HYP = " ^ (fst (print_context ey)));
         (*
         let time1 = Unix.gettimeofday() in
        let _, all_paths = NewConstraints.prefixes 5 ty in