]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/cicNotationTag.ml
added homepage URL, now we have one
[helm.git] / helm / ocaml / cic_notation / cicNotationTag.ml
index 67e966823944ade755f73f186bfc07c8a2ccbdd3..37579c82789d53e0e42d6ff839b98cb8e05c058f 100644 (file)
@@ -29,7 +29,6 @@ type tag = int
 type pattern_t = CicNotationPt.term
 
 let get_tag term0 =
-  prerr_endline "get_tag";
   let subterms = ref [] in
   let map_term t =
     subterms := t :: !subterms ; 
@@ -42,17 +41,5 @@ let get_tag term0 =
   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
-