Added a sort function to decide the order of theorems to try in the tactic "auto".

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

diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml
index 689102fe2439c982d94f756087375c2da6116c2e..e917555ce3e63f87a4052c224321f5416205f4c2 100644 (file)
--- a/helm/ocaml/tactics/tacticChaser.ml
+++ b/helm/ocaml/tactics/tacticChaser.ml
@@ -48,13 +48,11 @@ match list_of_must with
   [] -> []
 |_ ->
   let must = choose_must list_of_must only in
-   prerr_endline "123";
   let result =
    I.execute mqi_handle 
       (G.query_of_constraints
         (Some CGMatchConclusion.universe)
         (must,[],[]) (Some only,None,None)) in 
- prerr_endline "456";
   let uris =
    List.map
     (function uri,_ ->
@@ -140,9 +138,15 @@ let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() st
       not (suffix  = ".var") in
   let uris = List.filter isvar uris in
   (* delete all not "cic:/Coq" uris *)
+  (*
   let uris =
     (* TODO ristretto per ragioni di efficienza *)
-    List.filter (fun _,uri -> Pcre.pmatch ~pat:"^cic:/Coq/" uri) uris in 
+    List.filter (fun _,uri -> Pcre.pmatch ~pat:"^cic:/Coq/" uri) uris in
+  *)
+  (*
+  let uris =
+    List.filter  (fun _,uri -> not (Pcre.pmatch ~pat:"^cic:/Coq/ring" uri)) uris in
+  *)
   (* concl_cost are the costants in the conclusion of the proof 
      while hyp_const are the constants in the hypothesis *)
   let (_,concl_const) = NewConstraints.constants_of ty in