The universe was the one of the complete search, not that of the

searchPatter (restricted to the conclusion).

diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml
index 6f83c3fd67bb726d95fae43fe24e8fbada6b1f52..76a58091da7899dea84f55847538e6c383b16db9 100644 (file)
--- a/helm/ocaml/tactics/tacticChaser.ml
+++ b/helm/ocaml/tactics/tacticChaser.ml
@@ -52,8 +52,11 @@ let searchPattern mqi_handle ?(output_html = (fun _ -> ())) ~choose_must () ~sta
   let rigth_only = Some (List.map torigth_restriction only) in
   let result =
         MQueryInterpreter.execute mqi_handle 
-           (MQueryGenerator.query_of_constraints None
-               (rigth_must,[],[]) (rigth_only,None,None)) in 
+           (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"])
+        (rigth_must,[],[]) (rigth_only,None,None)) in 
        let uris =
         List.map
                (function uri,_ ->