]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/tactics/metadataQuery.ml
New functions UriManager.uri_is_var, UriManager.uri_is_con.
[helm.git] / helm / ocaml / tactics / metadataQuery.ml
index c1dd20ecc83badb808fb8e303b7feec3d701bbbf..ed4418dd2e5ef53eda901bf3d06a89ce1ea526c2 100644 (file)
@@ -43,11 +43,7 @@ let sqlpat_of_shellglob =
           (Pcre.replace ~rex:uscore_RE ~templ:"\\_"
             shellglob)))
 
-let nonvar s =
-  let s = UriManager.string_of_uri s in
-  let len = String.length s in
-  let suffix = String.sub s (len-4) 4 in
-  not (suffix  = ".var")
+let nonvar uri = not (UriManager.uri_is_var uri)
 
 let locate ~(dbd:Mysql.dbd) ?(vars = false) pat =
   let sql_pat = sqlpat_of_shellglob pat in