cicNotation* ==> notation*

[helm.git] / matita / components / grafite_engine / grafiteEngine.ml

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index a12a246aad04da223f4d33b9211a7e6e56fed935..e87795900c77bef72aee0ac6ffda9371695f8ac0 100644 (file)
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -543,7 +543,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
                try
                  let metasenv,subst,status,t =
                   GrafiteDisambiguate.disambiguate_nterm None status [] [] []
-                   ("",0,CicNotationPt.Ident (name,None)) in
+                   ("",0,NotationPt.Ident (name,None)) in
                  assert (metasenv = [] && subst = []);
                  let status, nuris = 
                    NCicCoercDeclaration.