]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/metadata/metadataTypes.ml
- changed metadata type so that positions contains depth
[helm.git] / helm / ocaml / metadata / metadataTypes.ml
index a5bbfaf097ad128f280fde538769b1a54907c6eb..719ba508c1ae37d5e40f364939c4dec35fe8658a 100644 (file)
  * http://helm.cs.unibo.it/
  *)
 
+let position_prefix = "http://www.cs.unibo.it/helm/schemas/schema-helm#"
+(* let position_prefix = "" *)
+
+let inconcl_pos = position_prefix ^ "InConclusion"
+let mainconcl_pos = position_prefix ^ "MainConclusion"
+let mainhyp_pos = position_prefix ^ "MainHypothesis"
+let inhyp_pos = position_prefix ^ "InHypothesis"
+let inbody_pos = position_prefix ^ "InBody"
+
 type main_position =
   [ `MainConclusion of int option (* Pi depth *)
   | `MainHypothesis of int option (* Pi depth *)