]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/ng_tactics/nTacStatus.ml
cicNotation* ==> notation*
[helm.git] / matita / components / ng_tactics / nTacStatus.ml
index 1aaeb50f6367ea58863034b8d12af18981203101..9f653abd51e63f2eb9b545fbf70112f261bc6e37 100644 (file)
@@ -48,7 +48,7 @@ class pstatus =
    = fun o -> (self#set_estatus o)#set_obj o#obj
   end
 
-type tactic_term = CicNotationPt.term Disambiguate.disambiguator_input
+type tactic_term = NotationPt.term Disambiguate.disambiguator_input
 type tactic_pattern = GrafiteAst.npattern Disambiguate.disambiguator_input
 
 let pp_tac_status status =