X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_generator%2FmQueryGenerator.ml;h=fd349c8ea8fdf0f87d3b065f5f7c9ac22bb909f6;hb=381006cf8b418cfdeaf145ab7df9e8f2b19ae2e6;hp=e56a744cd2cde7fd31ae2deda966520138dd6478;hpb=efdc3184ccd0738fe48aa0056fc444fba23329e8;p=helm.git

diff --git a/helm/ocaml/mathql_generator/mQueryGenerator.ml b/helm/ocaml/mathql_generator/mQueryGenerator.ml
index e56a744cd..fd349c8ea 100644
--- a/helm/ocaml/mathql_generator/mQueryGenerator.ml
+++ b/helm/ocaml/mathql_generator/mQueryGenerator.ml
@@ -44,20 +44,19 @@ let lamp xl      = M.Fun (["and"], [], xl)
 
 let locate s =
    let query = 
-      M.Property true M.RefineExact ["objectName"] [] [] [] []
-                 false (const s) 
+      M.Property (true, M.RefineExact, ["objectName"], [], [], [], [],
+                 false, (const s)) 
    in stat query
 
 let unreferred target_pattern source_pattern =
    let query = 
       diff 
       (
-         M.Property false M.RefineExact [] [] [] [] []
-                 true (const target_pattern) 
+         M.Property (false, M.RefineExact, [], [], [], [], [],
+                 true, (const target_pattern)) 
       ) (
-         M.Property false M.RefineExact ["refObj"] ["h:occurrence"] [] [] []
-                 true (const source_pattern) 
-      
+         M.Property (false, M.RefineExact, ["refObj"], ["h:occurrence"],
+	            [], [], [], true, (const source_pattern))
       )
    in stat query
 
@@ -91,13 +90,13 @@ let compose cl =
       con "h:depth" (List.map U.string_of_depth d)
    in
    let property_must n c =
-      M.Property true M.RefineExact [n] []
-	         (cons false c) [] [] false (const "") 
+      M.Property (true, M.RefineExact, [n], [],
+	         (cons false c), [], [], false, (const "")) 
    in   
    let property_only n cl =
       let cll = List.map (cons true) cl in
-      M.Property false M.RefineExact [n] []
-	         ! univ cll [] false (M.AVar "obj")
+      M.Property (false, M.RefineExact, [n], [],
+	         ! univ, cll, [], false, (M.AVar "obj"))
    in
    let rec aux = function 
       | [] -> ()
@@ -105,17 +104,17 @@ let compose cl =
          only := true; 
 	 let l = List.map U.string_of_position l in
 	 univ := [(false, ["h:position"], set_val l)]; aux tail 
-      | T.MustObj r p d :: tail ->
+      | T.MustObj (r, p, d) :: tail ->
          must := property_must "refObj" (r, [], p, d) :: ! must; aux tail  
-      | T.MustSort s p d :: tail ->
+      | T.MustSort (s, p, d) :: tail ->
 	 must := property_must "refSort" ([], s, p, d) :: ! must; aux tail 
-      | T.MustRel p d :: tail ->
+      | T.MustRel (p, d) :: tail ->
 	 must := property_must "refRel" ([], [], p, d) :: ! must; aux tail
-      | T.OnlyObj r p d :: tail ->
+      | T.OnlyObj (r, p, d) :: tail ->
 	 onlyobj := (r, [], p, d) :: ! onlyobj; aux tail
-      | T.OnlySort s p d :: tail ->
+      | T.OnlySort (s, p, d) :: tail ->
          onlysort := ([], s, p, d) :: ! onlysort; aux tail
-      | T.OnlyRel p d :: tail ->
+      | T.OnlyRel (p, d) :: tail ->
          onlyrel := ([], [], p, d) :: ! onlyrel; aux tail
    in
    let rec iter f g = function
@@ -128,7 +127,8 @@ let compose cl =
    aux cl;
    let must_query =
       if ! must = [] then  
-         M.Property false M.RefineExact [] [] [] [] [] true (const ".*")
+         M.Property (false, M.RefineExact, [], [], 
+	             [], [], [], true, (const ".*"))
       else 
          intersect ! must   
    in