X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_notation%2FcicNotationTag.ml;h=37579c82789d53e0e42d6ff839b98cb8e05c058f;hb=3eff4cc36820df9faddb3cb16390717851db499c;hp=b454cf24df3508c00ae21e29e0558363dbdd2edf;hpb=3d63cb9ed38f05c679fc3284a5b3bb4d92e52296;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationTag.ml b/helm/ocaml/cic_notation/cicNotationTag.ml
index b454cf24d..37579c827 100644
--- a/helm/ocaml/cic_notation/cicNotationTag.ml
+++ b/helm/ocaml/cic_notation/cicNotationTag.ml
@@ -43,14 +43,3 @@ let get_tag term0 =
   let tag = Hashtbl.hash term_mask in
   tag, !subterms
 
-let compatible t1 t2 =
-  match t1, t2 with
-  | Variable _, Variable _ -> true
-  | Variable _, _
-  | _, Variable _
-  | Magic _, _
-  | _, Magic _ -> false
-  | Layout _, _
-  | _, Layout _ -> assert false
-  | _ -> true
-