X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_generator%2FmQueryGenerator.ml;h=2d529c9e8aa32f9f23659bebafcc418706bc5378;hb=931f10c61b4e3914474955a94a05cf43b5fa2bc0;hp=24720d0aab4c9a4051168f7cd6218147a393ed90;hpb=210445db4d7f550bbfac3e2db6d0aefcf02b71d4;p=helm.git

diff --git a/helm/ocaml/mathql_generator/mQueryGenerator.ml b/helm/ocaml/mathql_generator/mQueryGenerator.ml
index 24720d0aa..2d529c9e8 100644
--- a/helm/ocaml/mathql_generator/mQueryGenerator.ml
+++ b/helm/ocaml/mathql_generator/mQueryGenerator.ml
@@ -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,6 +39,15 @@ 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
+
 let text_of_builtin s =
    let ns = "http://www.cs.unibo.it/helm/schemas/schema-helm#" in
    if s = ns ^ "MainHypothesis" then "$MH" else
@@ -43,9 +55,9 @@ let text_of_builtin s =
    if s = ns ^ "MainConclusion" then "$MC" else
    if s = ns ^ "InConclusion" then "$IC" else
    if s = ns ^ "InBody" then "$IB" else
-   if s = ns ^ "Set" then "$SET" else
-   if s = ns ^ "Prop" then "$PROP" else
-   if s = ns ^ "Type" then "$TYPE" else s
+   if s =      "Set" then "$SET" else
+   if s =      "Prop" then "$PROP" else
+   if s =      "Type" then "$TYPE" else s
 
 let text_of_spec out l =
    let rec iter = function 
@@ -164,15 +176,14 @@ let compose cl =
 let builtin s = 
    let ns = "http://www.cs.unibo.it/helm/schemas/schema-helm#" in
    match s with
-      | "MH"   -> ns ^ "MainHypothesis"
-      | "IH"   -> ns ^ "InHypothesis"
-      | "MC"   -> ns ^ "MainConclusion"
-      | "IC"   -> ns ^ "InConclusion"
-      | "IB"   -> ns ^ "InBody"
-      | "SET"  -> ns ^ "Set"
-      | "PROP" -> ns ^ "Prop"
-      | "TYPE" -> ns ^ "Type"
-      | _      -> raise (Failure "MQueryGenerator.builtin")
+      | MainHypothesis -> ns ^ "MainHypothesis"
+      | InHypothesis   -> ns ^ "InHypothesis"
+      | MainConclusion -> ns ^ "MainConclusion"
+      | InConclusion   -> ns ^ "InConclusion"
+      | InBody         -> ns ^ "InBody"
+      | Set            ->      "Set"
+      | Prop           ->      "Prop"
+      | Type           ->      "Type"
 
 (* conversion functions from the old constraints  ***************************)