X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_generator%2FmQueryGenerator.mli;h=decaa0ea761be56f337c1b67a7d4cd02f33e1cf3;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=6081cd02802819a92a06ca3520ff5a156717adeb;hpb=931f10c61b4e3914474955a94a05cf43b5fa2bc0;p=helm.git

diff --git a/helm/ocaml/mathql_generator/mQueryGenerator.mli b/helm/ocaml/mathql_generator/mQueryGenerator.mli
index 6081cd028..decaa0ea7 100644
--- a/helm/ocaml/mathql_generator/mQueryGenerator.mli
+++ b/helm/ocaml/mathql_generator/mQueryGenerator.mli
@@ -26,45 +26,17 @@
 (*  AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
  *)
 
-type uri = string
-type position = string
-type depth = string
-type sort = string 
+(* interface for the low-level constraints  *********************************)
 
-type spec = MustObj  of uri list * position list * depth list
-          | MustSort of sort list * position list * depth list
-          | MustRel  of position list * depth list
-          | OnlyObj  of uri list * position list * depth list
-          | OnlySort of sort list * position list * depth list
-          | OnlyRel  of position list * depth list
-          | Universe of position list 
+val locate     : string -> MathQL.query
 
-type builtin_t = MainHypothesis
-               | InHypothesis
-	       | MainConclusion
-	       | InConclusion
-	       | InBody
-	       | Set
-	       | Prop
-	       | Type
+val unreferred : string -> string -> MathQL.query
 
-val locate  : string -> MathQL.query
+val compose    : MQGTypes.spec list -> MathQL.query
 
-val compose : spec list -> MathQL.query
+(* interface for the high-level constraints  ********************************)
 
-val builtin : builtin_t -> string
-
-(* interface for the old constraints  ***************************************)
-
-type old_depth = int option
- 
-type r_obj = uri * position * old_depth 
-type r_rel = position * old_depth
-type r_sort = position * old_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)
-type universe = position list option
-
-val query_of_constraints : universe -> must_restrictions -> only_restrictions -> MathQL.query
+val query_of_constraints : MQGTypes.universe option -> 
+                           MQGTypes.must_restrictions ->
+                           MQGTypes.only_restrictions -> 
+			   MathQL.query