]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/searchEngine/searchEngine.ml
http://....#Prop shortened to Prop due to a bug (feature?) in the DB.
[helm.git] / helm / searchEngine / searchEngine.ml
index 13331c27be7d4748e70136627157472c1fe98a84..ca507663511a7696d2b182064c3ba4ab94d783cb 100644 (file)
@@ -236,7 +236,7 @@ let get_constraints term =
         None] in
       let constr_sort =
        ["http://www.cs.unibo.it/helm/schemas/schema-helm#MainHypothesis",
-        Some 1, "http://www.cs.unibo.it/helm/schemas/schema-helm#Prop"]
+        Some 1, "Prop"]
       in
        whole_statement_universe,
         (constr_obj, constr_rel, constr_sort), (None,None,None)