X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationTag.ml;h=3cbffa2db885425ebc2ee84946ba9caf4eee5159;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;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..3cbffa2db 100644
--- a/helm/ocaml/cic_notation/cicNotationTag.ml
+++ b/helm/ocaml/cic_notation/cicNotationTag.ml
@@ -23,34 +23,23 @@
  * http://helm.cs.unibo.it/
  *)
 
-open CicNotationPt
+module Ast = CicNotationPt
 
 type tag = int
-type pattern_t = CicNotationPt.term
+type pattern_t = Ast.term
 
 let get_tag term0 =
   let subterms = ref [] in
   let map_term t =
     subterms := t :: !subterms ; 
-    Implicit
+    Ast.Implicit
   in
   let rec aux t = CicNotationUtil.visit_ast ~special_k map_term t
   and special_k = function
-    | AttributedTerm (_, t) -> aux t
+    | Ast.AttributedTerm (_, t) -> aux t
     | _ -> assert false
   in
   let term_mask = aux term0 in
   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
+  tag, List.rev !subterms