From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 20 Apr 2005 16:47:32 +0000 (+0000)
Subject: bugfixes:
X-Git-Tag: after_svn_merge~32
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=15b9864a7b1397ab76f69a2f9c7458f3362fa3db;p=helm.git

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 73e6f288d..ab8c00f99 100644
--- 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