]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/cicNotationTag.ml
version 0.7.1
[helm.git] / helm / ocaml / cic_notation / cicNotationTag.ml
index 67e966823944ade755f73f186bfc07c8a2ccbdd3..b454cf24df3508c00ae21e29e0558363dbdd2edf 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,16 @@ 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 _
+  | _, Variable _
   | Magic _, _
-  | _, Magic _ -> assert false
+  | _, Magic _ -> false
+  | Layout _, _
+  | _, Layout _ -> assert false
   | _ -> true