implemented transformations on top of notation code

[helm.git] / helm / ocaml / cic_notation / cicNotationTag.ml

diff --git a/helm/ocaml/cic_notation/cicNotationTag.ml b/helm/ocaml/cic_notation/cicNotationTag.ml
index b454cf24df3508c00ae21e29e0558363dbdd2edf..37579c82789d53e0e42d6ff839b98cb8e05c058f 100644 (file)
--- 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
-