* 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
+ tag, List.rev !subterms