]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/grafite/grafiteAstPp.ml
1. matitaEngine splitted into disambiguation (now in grafite_parser) and
[helm.git] / helm / ocaml / grafite / grafiteAstPp.ml
index 28f42ca6d5eb4e7f1bc7a234598aa5138ca44919..7687bc5222235543bd6da28bd876f6253710b54f 100644 (file)
@@ -27,8 +27,6 @@ open Printf
 
 open GrafiteAst
 
-module Ast = CicNotationPt
-
 let tactical_terminator = ""
 let tactic_terminator = tactical_terminator
 let command_terminator = tactical_terminator
@@ -186,7 +184,7 @@ let pp_alias = function
       sprintf "alias num (instance %d) = \"%s\"" instance desc
   
 let pp_argument_pattern = function
-  | Ast.IdentArg (eta_depth, name) ->
+  | CicNotationPt.IdentArg (eta_depth, name) ->
       let eta_buf = Buffer.create 5 in
       for i = 1 to eta_depth do
         Buffer.add_string eta_buf "\\eta."