X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationTag.mli;h=bf04e0a9fa8929b3399445193e01c6abf0b37543;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=62f9ca091e5a787a16cc59f8914870d78cef8e97;hpb=dbcc29c0e46454c7e31b485135900ceab38627e1;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationTag.mli b/helm/ocaml/cic_notation/cicNotationTag.mli
index 62f9ca091..bf04e0a9f 100644
--- a/helm/ocaml/cic_notation/cicNotationTag.mli
+++ b/helm/ocaml/cic_notation/cicNotationTag.mli
@@ -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