From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 19 Jun 2003 17:49:21 +0000 (+0000)
Subject: The universe was the one of the complete search, not that of the
X-Git-Tag: V7_3_new_exportation_merged~11
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a8f512296b650595549fe3e125930657d20bb99c;p=helm.git

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 6f83c3fd6..76a58091d 100644
--- 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,_ ->