type pattern_t = CicNotationPt.term
let get_tag term0 =
- prerr_endline "get_tag";
let subterms = ref [] in
let map_term t =
subterms := t :: !subterms ;
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