]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/ng_tactics/nTactics.ml
cicNotation* ==> notation*
[helm.git] / matita / components / ng_tactics / nTactics.ml
index c45e825a40359ff75fbe464416d19d9bc692760c..09427a315d6ca3f99b3c57c5091410e09df6c21c 100644 (file)
@@ -18,7 +18,7 @@ let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
 
 open Continuationals.Stack
 open NTacStatus
-module Ast = CicNotationPt
+module Ast = NotationPt
 
 let id_tac status = status ;;
 let print_tac print_status message status =