]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/cicNotationTag.mli
ocaml 3.09 transition
[helm.git] / helm / ocaml / cic_notation / cicNotationTag.mli
index 62f9ca091e5a787a16cc59f8914870d78cef8e97..bf04e0a9fa8929b3399445193e01c6abf0b37543 100644 (file)
@@ -23,9 +23,5 @@
  * http://helm.cs.unibo.it/
  *)
 
-type tag = int
-type pattern_t = CicNotationPt.term
-
-val get_tag: pattern_t -> tag * pattern_t list
-val compatible: pattern_t -> pattern_t -> bool
+val get_tag: CicNotationPt.term -> int * CicNotationPt.term list