mathql_interpreter: natile-galax package removed from Makefie and META

[helm.git] / helm / ocaml / mathql_generator / mQueryLevels2.ml

diff --git a/helm/ocaml/mathql_generator/mQueryLevels2.ml b/helm/ocaml/mathql_generator/mQueryLevels2.ml
index 968d2a35e8d6439c65c0549bc35d7f58c372f383..d9e9e5359276095df3633f055abe48c507daaa6b 100644 (file)
--- a/helm/ocaml/mathql_generator/mQueryLevels2.ml
+++ b/helm/ocaml/mathql_generator/mQueryLevels2.ml
@@ -87,12 +87,9 @@ let get_constraints term =
          | Branch _ ->
             let s' =
              match s with
-                Cic.Prop ->
-                 "http://www.cs.unibo.it/helm/schemas/schema-helm#Prop"
-              | Cic.Set ->
-                 "http://www.cs.unibo.it/helm/schemas/schema-helm#Set"
-              | Cic.Type ->
-                 "http://www.cs.unibo.it/helm/schemas/schema-helm#Type"
+                Cic.Prop -> "Prop"
+              | Cic.Set -> "Set"
+              | Cic.Type -> "Type"
             in
              let kind',depth = !!kind in
               (match depth with