cicNotation* ==> notation*

[helm.git] / matita / components / ng_tactics / nTacStatus.mli

diff --git a/matita/components/ng_tactics/nTacStatus.mli b/matita/components/ng_tactics/nTacStatus.mli
index 5616794573ed830c42ab14913de5a61501f90d78..a51435e24d3eceba991eb49c48d38fd56567c4e2 100644 (file)
--- a/matita/components/ng_tactics/nTacStatus.mli
+++ b/matita/components/ng_tactics/nTacStatus.mli
@@ -29,7 +29,7 @@ class pstatus :
    method set_pstatus: #g_pstatus -> 'self
   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
 
 type cic_term