]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/cicNotationTag.ml
ocaml 3.09 transition
[helm.git] / helm / ocaml / cic_notation / cicNotationTag.ml
index 37579c82789d53e0e42d6ff839b98cb8e05c058f..3cbffa2db885425ebc2ee84946ba9caf4eee5159 100644 (file)
  * 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