debian: rebuilt against ocaml 3.08.3

[helm.git] / helm / ocaml / tactics / metadataQuery.ml

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index 4e6b31b537ce880232b591cccc3f9197bd8726dc..8dcbcd08abd3e3d9d0d585c4aa390c46223e4e89 100644 (file)
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -46,23 +46,13 @@ let nonvar s =
   let suffix = String.sub s (len-4) 4 in
   not (suffix  = ".var")
 
-let locate ~(dbd:Mysql.dbd) ?(vars = false) ?owner pat =
+let locate ~(dbd:Mysql.dbd) ?(vars = false) pat =
   let sql_pat = sqlpat_of_shellglob pat in
   let query =
-    match owner with
-    | None -> 
-        sprintf "SELECT source FROM %s WHERE value LIKE \"%s\""
-          MetadataTypes.name_tbl sql_pat
-    | Some owner -> 
-        sprintf "SELECT %s.source FROM %s,%s WHERE 
-                  (%s.source LIKE CONCAT(%s.source,\"#%%\") OR 
-                   %s.source = %s.source) AND
-                  value LIKE \"%s\" AND owner = \"%s\""
-          MetadataTypes.name_tbl
-          MetadataTypes.name_tbl MetadataTypes.owners_tbl
-          MetadataTypes.name_tbl MetadataTypes.owners_tbl
-          MetadataTypes.name_tbl MetadataTypes.owners_tbl
-          sql_pat owner
+        sprintf ("SELECT source FROM %s WHERE value LIKE \"%s\" UNION "^^
+                 "SELECT source FROM %s WHERE value LIKE \"%s\"")
+          (MetadataTypes.name_tbl ()) sql_pat
+           MetadataTypes.library_name_tbl sql_pat
   in
   let result = Mysql.exec dbd query in
   List.filter nonvar
@@ -74,9 +64,16 @@ let match_term ~(dbd:Mysql.dbd) ty =
   let constants_no =
     MetadataConstraints.StringSet.cardinal (MetadataConstraints.constants_of ty)
   in
+  let full_card =
+    if CicUtil.is_meta_closed ty then
+      Some (MetadataConstraints.Eq constants_no)
+    else
+      None  (* we already require a set of constants to appear, this additional
+             constraints is useless *)
+(*       MetadataConstraints.Gt (constants_no - 1) *)
+  in
   let constraints = List.map MetadataTypes.constr_of_metadata metadata in
-  Constr.at_least ~dbd ~full_card:(MetadataConstraints.Eq constants_no)
-    constraints
+  Constr.at_least ~dbd ?full_card constraints
 
 let ( ** ) x y = int_of_float ((float_of_int x) ** (float_of_int y))
 
@@ -164,7 +161,7 @@ let hint ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
   let hyp_constants =
     Constr.StringSet.diff (signature_of_hypothesis context) types_constants
   in
-Constr.StringSet.iter prerr_endline hyp_constants;
+(* Constr.StringSet.iter prerr_endline hyp_constants; *)
   let other_constants = Constr.StringSet.union sig_constants hyp_constants in
   let uris = 
     let pow = 2 ** (Constr.StringSet.cardinal other_constants) in
@@ -235,7 +232,7 @@ let experimental_hint
   let hyp_constants =
     Constr.StringSet.diff (signature_of_hypothesis context) types_constants
   in
-Constr.StringSet.iter prerr_endline hyp_constants;
+(* Constr.StringSet.iter prerr_endline hyp_constants; *)
   let other_constants = Constr.StringSet.union sig_constants hyp_constants in
   let uris = 
     let pow = 2 ** (Constr.StringSet.cardinal other_constants) in