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

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