X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FvariousTactics.ml;h=f8c9cfa94dd409b67f65cbbfe332681473978eef;hb=6150b8ef905aaea17b47ff466c067054f976cd8f;hp=bb5be64d8837a8592560ecaf7ef8a3f6072672e1;hpb=bd59745a232bff0e941e97170b88709d0ff6fdf2;p=helm.git

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index bb5be64d8..f8c9cfa94 100644
--- 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