From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 29 Jun 2003 18:28:58 +0000 (+0000)
Subject: mathql_interpreter: natile-galax package removed from Makefie and META
X-Git-Tag: camera_ready~35
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=20595b27aa778b574d2f8ab5edaa1aa0382e01c5

mathql_interpreter: natile-galax package removed from Makefie and META
mathql_generator  : MQueryLevels2.ml patched (namespaces removed from sorts)
---

diff --git a/helm/ocaml/META.helm-mathql_interpreter.src b/helm/ocaml/META.helm-mathql_interpreter.src
index 1806188c3..24a192956 100644
--- a/helm/ocaml/META.helm-mathql_interpreter.src
+++ b/helm/ocaml/META.helm-mathql_interpreter.src
@@ -1,4 +1,5 @@
-requires="helm-cic helm-cic_textual_parser postgres natile-galax helm-mathql"
+requires="helm-cic helm-cic_textual_parser postgres helm-mathql"
+#natile-galax 
 version="1.3"
 archive(byte)="mathql_interpreter.cma"
 archive(native)="mathql_interpreter.cmxa"
diff --git a/helm/ocaml/mathql_generator/mQueryLevels2.ml b/helm/ocaml/mathql_generator/mQueryLevels2.ml
index 968d2a35e..d9e9e5359 100644
--- 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
diff --git a/helm/ocaml/mathql_interpreter/Makefile b/helm/ocaml/mathql_interpreter/Makefile
index 929f149e1..18fcd5512 100644
--- a/helm/ocaml/mathql_interpreter/Makefile
+++ b/helm/ocaml/mathql_interpreter/Makefile
@@ -1,6 +1,6 @@
 PACKAGE = mathql_interpreter
-REQUIRES = helm-cic helm-cic_textual_parser \
-	   postgres natile-galax helm-mathql
+REQUIRES = helm-cic helm-cic_textual_parser helm-mathql postgres
+#natile-galax 
 
 PREDICATES =