mathql_generator: new constraint format (more type safe)

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

diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml
index 76a58091da7899dea84f55847538e6c383b16db9..c4bfc5e034f17b170a387e28216a92556f0febd6 100644 (file)
--- a/helm/ocaml/tactics/tacticChaser.ml
+++ b/helm/ocaml/tactics/tacticChaser.ml
@@ -33,29 +33,25 @@
 (*                                                                            *)
 (******************************************************************************)
 
+module I = MQueryInterpreter
+module U = MQGUtil
+module G = MQueryGenerator
+
   (* search arguments on which Apply tactic doesn't fail *)
-let searchPattern mqi_handle ?(output_html = (fun _ -> ())) ~choose_must () ~status =
+let matchConclusion mqi_handle ?(output_html = (fun _ -> ())) ~choose_must () ~status =
  let ((_, metasenv, _, _), metano) = status in
  let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
   let list_of_must,only = MQueryLevels.out_restr metasenv ey ty in
   let must = choose_must list_of_must only in
   let torigth_restriction (u,b) =
-   let p =
-    if b then
-     "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion" 
-    else
-     "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion"
-    in
-    (u,p,None)
+   (if b then `MainConclusion None else `InConclusion), u
   in
   let rigth_must = List.map torigth_restriction must in
   let rigth_only = Some (List.map torigth_restriction only) in
   let result =
-        MQueryInterpreter.execute mqi_handle 
-           (MQueryGenerator.query_of_constraints
-        (Some
-          ["http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion" ;
-           "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion"])
+        I.execute mqi_handle 
+           (G.query_of_constraints
+        (Some U.universe_for_match_conclusion)
         (rigth_must,[],[]) (rigth_only,None,None)) in 
        let uris =
         List.map