]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql_generator/mQueryGenerator.ml
- patched for new CIC
[helm.git] / helm / ocaml / mathql_generator / mQueryGenerator.ml
index fd349c8ea8fdf0f87d3b065f5f7c9ac22bb909f6..7b72045638810878b35ce8c535b936951a949672 100644 (file)
@@ -32,7 +32,6 @@ module U = MQGUtil
 
 (* helpers  *****************************************************************)
 
-let stat x       = M.Fun (["stat"], [], [x])
 let diff x y     = M.Fun (["diff"], [], [x; y])
 let union xl     = M.Fun (["union"], [], xl)
 let const s      = M.Const [(s, [])]
@@ -46,7 +45,7 @@ let locate s =
    let query = 
       M.Property (true, M.RefineExact, ["objectName"], [], [], [], [],
                  false, (const s)) 
-   in stat query
+   in query
 
 let unreferred target_pattern source_pattern =
    let query = 
@@ -58,7 +57,7 @@ let unreferred target_pattern source_pattern =
          M.Property (false, M.RefineExact, ["refObj"], ["h:occurrence"],
                    [], [], [], true, (const source_pattern))
       )
-   in stat query
+   in query
 
 let compose cl = 
    let letin = ref [] in
@@ -152,7 +151,7 @@ let compose cl =
         let f (vvar, msval) x = M.Let (Some vvar, msval, x) in 
         iter f (fun x y z -> x (y z)) ! letin
    in 
-   stat (letin_query (select_query must_query))
+   letin_query (select_query must_query)
 
 (* high-level functions  ****************************************************)