X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_generator%2FmQueryGenerator.mli;h=c94dbcdb87809d376738b63caaf08bdb5c8f02a9;hb=a48c5f0f412bbb8c1d6601dd5e11e5c3746f11d5;hp=6081cd02802819a92a06ca3520ff5a156717adeb;hpb=3c7ca719c304eb7de7d8d4e9a90ebe0db8d8ecab;p=helm.git

diff --git a/helm/ocaml/mathql_generator/mQueryGenerator.mli b/helm/ocaml/mathql_generator/mQueryGenerator.mli
index 6081cd028..c94dbcdb8 100644
--- a/helm/ocaml/mathql_generator/mQueryGenerator.mli
+++ b/helm/ocaml/mathql_generator/mQueryGenerator.mli
@@ -23,9 +23,6 @@
  * http://cs.unibo.it/helm/.
  *)
 
-(*  AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
 type uri = string
 type position = string
 type depth = string
@@ -33,26 +30,17 @@ type sort = string
 
 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
+	  | 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 
-
-type builtin_t = MainHypothesis
-               | InHypothesis
-	       | MainConclusion
-	       | InConclusion
-	       | InBody
-	       | Set
-	       | Prop
-	       | Type
+	  | OnlyRel  of position list * depth list
+	  | Universe of position list 
 
 val locate  : string -> MathQL.query
 
 val compose : spec list -> MathQL.query
 
-val builtin : builtin_t -> string
+val builtin : MathQL.vvar -> string
 
 (* interface for the old constraints  ***************************************)