Bug in the management of substitutions into auto corrected.

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

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index bb5594a35693f50917f86516419df44858e373b0..e5656b9b3f9aaa80e9e68c2b1169cad747ff7958 100644 (file)
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -126,7 +126,6 @@ let hint ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
   let hyp_constants =
     Constr.StringSet.diff (signature_of_hypothesis context) types_constants
   in
-prerr_endline "HYP SIGNATURE";
 Constr.StringSet.iter prerr_endline hyp_constants;
   let other_constants = Constr.StringSet.union sig_constants hyp_constants in
   let uris = 
@@ -144,7 +143,7 @@ Constr.StringSet.iter prerr_endline hyp_constants;
         (let status' =
             try
               let (proof, goal_list) =
-                prerr_endline ("STO APPLICANDO " ^ uri);
+(*                prerr_endline ("STO APPLICANDO " ^ uri); *)
                PET.apply_tactic
                   (PrimitiveTactics.apply_tac
                    ~term:(CicUtil.term_of_uri uri))
@@ -198,7 +197,6 @@ let experimental_hint
   let hyp_constants =
     Constr.StringSet.diff (signature_of_hypothesis context) types_constants
   in
-prerr_endline "HYP SIGNATURE";
 Constr.StringSet.iter prerr_endline hyp_constants;
   let other_constants = Constr.StringSet.union sig_constants hyp_constants in
   let uris = 
@@ -216,7 +214,7 @@ Constr.StringSet.iter prerr_endline hyp_constants;
         (let status' =
             try
               let (subst,(proof, goal_list)) =
-                  prerr_endline ("STO APPLICANDO" ^ uri);
+                  (* prerr_endline ("STO APPLICANDO" ^ uri); *)
                   PrimitiveTactics.apply_tac_verbose 
                    ~term:(CicUtil.term_of_uri uri)
                   status