bugfixes:

- reference position using MetadataTypes.*_pos so that changing the
  position prefix fixes all the references
- don't generated dummy predicates which always suceed like ("mainConcl" OR
  "inConcl") for at_most checking

diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml
index 73e6f288dfd3b4e3b5815842684177d929a92717..ab8c00f9981c81d1c0bcdeaa8370ee22dff13795 100644 (file)
--- a/helm/ocaml/metadata/metadataConstraints.ml
+++ b/helm/ocaml/metadata/metadataConstraints.ml
@@ -398,16 +398,20 @@ let get_constants (dbd:Mysql.dbd) ~where uri =
   let uri = escape uri in
   let positions =
     match where with
-    | `Conclusion -> ["\"MainConclusion\""; "\"InConclusion\""]
+    | `Conclusion -> [ MetadataTypes.mainconcl_pos; MetadataTypes.inconcl_pos ]
     | `Statement ->
-        ["\"MainConclusion\""; "\"InConclusion\""; "\"InHypothesis\"";
-         "\"MainHypothesis\""]
+        [ MetadataTypes.mainconcl_pos; MetadataTypes.inconcl_pos;
+          MetadataTypes.inhyp_pos; MetadataTypes.mainhyp_pos ]
   in
   let query = 
+    let pos_predicate =
+      String.concat " OR "
+        (List.map (fun pos -> sprintf "(h_position = \"%s\")" pos) positions)
+    in
     sprintf ("SELECT h_occurrence FROM %s WHERE source=\"%s\" AND (%s) UNION "^^
              "SELECT h_occurrence FROM %s WHERE source=\"%s\" AND (%s)")
-      (MetadataTypes.obj_tbl ()) uri (String.concat " OR " positions)
-      MetadataTypes.library_obj_tbl uri (String.concat " OR " positions)
+      (MetadataTypes.obj_tbl ()) uri pos_predicate
+      MetadataTypes.library_obj_tbl uri pos_predicate
       
   in
   let result = Mysql.exec dbd query in