X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_generator%2FmQueryGenerator.ml;h=40c0ea0b8372dc063f79f4087ccde41aaa04c310;hb=96134b9ec1030ed15cea00d751dd4d744463f62c;hp=1a0211102b782552daa204c60e8c370e6f35d59b;hpb=12dd0be29a6a7dc6ac7a571fa99e2aa728fce4d2;p=helm.git

diff --git a/helm/ocaml/mathql_generator/mQueryGenerator.ml b/helm/ocaml/mathql_generator/mQueryGenerator.ml
index 1a0211102..40c0ea0b8 100644
--- a/helm/ocaml/mathql_generator/mQueryGenerator.ml
+++ b/helm/ocaml/mathql_generator/mQueryGenerator.ml
@@ -38,6 +38,19 @@ let locate s =
                  false (M.Const s) 
    in M.StatQuery query
 
+let unreferred target_pattern source_pattern =
+   let query = 
+      M.Bin M.BinFDiff
+      (
+         M.Property false M.RefineExact [] [] [] [] []
+                 true (M.Const target_pattern) 
+      ) (
+         M.Property false M.RefineExact ["refObj"] ["h:occurrence"] [] [] []
+                 true (M.Const source_pattern) 
+      
+      )
+   in M.StatQuery query
+
 let compose cl = 
    let letin = ref [] in
    let must = ref [] in
@@ -100,7 +113,8 @@ let compose cl =
       | [head]       -> (f head) 
       | head :: tail -> let t = (iter f g tail) in g (f head) t
    in
-   U.mathql_of_specs prerr_string cl;
+   prerr_endline "(** Compose: received constraints **)";
+   U.mathql_of_specs prerr_string cl; flush stderr;
    aux cl;
    let must_query =
       if ! must = [] then