Author specification added in head comments;

[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 9229290e86511633095facbd8fb1f65979c096f1..6081cd02802819a92a06ca3520ff5a156717adeb 100644 (file)
--- a/helm/ocaml/mathql_generator/mQueryGenerator.mli
+++ b/helm/ocaml/mathql_generator/mQueryGenerator.mli
@@ -23,6 +23,9 @@
  * http://cs.unibo.it/helm/.
  *)
 
+(*  AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
 type uri = string
 type position = string
 type depth = string
@@ -36,11 +39,20 @@ type spec = MustObj  of uri 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
+
 val locate  : string -> MathQL.query
 
 val compose : spec list -> MathQL.query
 
-val builtin : MathQL.vvar -> string
+val builtin : builtin_t -> string
 
 (* interface for the old constraints  ***************************************)