X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationTag.ml;h=3cbffa2db885425ebc2ee84946ba9caf4eee5159;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=67e966823944ade755f73f186bfc07c8a2ccbdd3;hpb=dbcc29c0e46454c7e31b485135900ceab38627e1;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationTag.ml b/helm/ocaml/cic_notation/cicNotationTag.ml
index 67e966823..3cbffa2db 100644
--- a/helm/ocaml/cic_notation/cicNotationTag.ml
+++ b/helm/ocaml/cic_notation/cicNotationTag.ml
@@ -23,36 +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 =
-  prerr_endline "get_tag";
   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
-  Printf.printf "TAG = %d\n" tag ; flush stdout ;
-  tag, !subterms
-
-let compatible t1 t2 =
-  match t1, t2 with
-  | Variable _, Variable _ -> true
-  | Variable _, _
-  | _, Variable _ -> false
-  | Layout _, _
-  | _, Layout _
-  | Magic _, _
-  | _, Magic _ -> assert false
-  | _ -> true
+  tag, List.rev !subterms