X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FmQueryGenerator.mli;h=b1db11142a9c0920e63d16319d1b18a91d67f1c1;hb=370f967a478c116fcc85a81c7953363b4351a2e9;hp=57137974f8ad0d7e12b88273ebcb956d4bd5fcbf;hpb=86122a3ce11bdf45ecb93f8f7efaffa49bd31fa2;p=helm.git

diff --git a/helm/gTopLevel/mQueryGenerator.mli b/helm/gTopLevel/mQueryGenerator.mli
index 57137974f..b1db11142 100644
--- a/helm/gTopLevel/mQueryGenerator.mli
+++ b/helm/gTopLevel/mQueryGenerator.mli
@@ -35,11 +35,20 @@
 
 exception Discard  
 
-type levels_spec = (string * bool * int) list
+type uri = string
+type position = string
+type depth = int option
+type sort = string 
+
+type r_obj = (uri * position * depth) 
+type r_rel = (position * depth)
+type r_sort = (position * depth * sort) 
+
+type must_restrictions = (r_obj list * r_rel list * r_sort list)
+type only_restrictions =
+ (r_obj list option * r_rel list option * r_sort list option)
 
-val levels_of_term    : Cic.metasenv -> Cic.context -> Cic.term -> levels_spec
 
-val string_of_levels  : levels_spec -> string -> string
 
 val set_log_file      : string -> unit
 
@@ -50,6 +59,6 @@ val execute_query     : MathQL.query -> MathQL.result
 
 val locate            : string -> MathQL.result
 
-val backward          : Cic.metasenv -> Cic.context -> Cic.term -> int -> MathQL.result
+val searchPattern     : must_restrictions -> only_restrictions -> MathQL.result
 
 val get_query_info    : unit -> string list