]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/metadata/metadataTypes.ml
implemented here at_least constraints matching engine
[helm.git] / helm / ocaml / metadata / metadataTypes.ml
index dbe94695e0a8f707898c2940f02d041fb3ac7a47..0db48f299dde415b8e8584556527d163167f8a8f 100644 (file)
@@ -40,3 +40,11 @@ type metadata =
   | `Obj of string * position * pi_depth option
   ]
 
+let sort_tbl = "refSort"
+let rel_tbl = "refRel"
+let obj_tbl = "refObj"
+let owners_tbl = "owners"
+let conclno_tbl = "no_inconcl_aux"
+let conclno_hyp_tbl = "no_concl_hyp"
+let name_tbl = "objectName"
+