X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_generator%2FmQueryGenerator.ml;h=dd8b00ae327aeb0248acc88a92024046320b7051;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=7175eb6153179519a714a1dc22075a75d6bb48c0;hpb=dcc98e7121fef75c9244a80427d036b312632d0d;p=helm.git diff --git a/helm/ocaml/mathql_generator/mQueryGenerator.ml b/helm/ocaml/mathql_generator/mQueryGenerator.ml index 7175eb615..dd8b00ae3 100644 --- a/helm/ocaml/mathql_generator/mQueryGenerator.ml +++ b/helm/ocaml/mathql_generator/mQueryGenerator.ml @@ -81,7 +81,13 @@ let compose cl = M.Property(true,M.RefineExact,[n],[],(cons false c),[],[],false,(M.Const "")) in let property_only n cl = - let cll = List.map (cons true) cl in + let rec build = function + | [] -> [] + | c :: tl -> + let r = (cons true) c in + if r = [] then build tl else r :: build tl + in + let cll = build cl in M.Property(false,M.RefineExact,[n],[],!univ,cll,[],false,(M.Proj(None,(M.AVar "obj")))) in let rec aux = function @@ -108,8 +114,8 @@ let compose cl = | [head] -> (f head) | head :: tail -> let t = (iter f g tail) in g (f head) t in - prerr_endline "(** Compose: received constraints **)"; - U.mathql_of_specs prerr_string cl; flush stderr; + (* prerr_endline "(** Compose: received constraints **)"; + U.mathql_of_specs prerr_string cl; flush stderr; *) aux cl; let must_query = if ! must = [] then