This commit was manufactured by cvs2svn to create tag

[helm.git] / helm / ocaml / mathql_generator / mQueryGenerator.mli

diff --git a/helm/ocaml/mathql_generator/mQueryGenerator.mli b/helm/ocaml/mathql_generator/mQueryGenerator.mli
index 6081cd02802819a92a06ca3520ff5a156717adeb..c94dbcdb87809d376738b63caaf08bdb5c8f02a9 100644 (file)
--- 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  ***************************************)