X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=e87795900c77bef72aee0ac6ffda9371695f8ac0;hb=8a660ee06d72cfee52c707bb1d8d8be3bab0d682;hp=a12a246aad04da223f4d33b9211a7e6e56fed935;hpb=5553ac7623425bce6f34eed6e17d4f0f8163e9aa;p=helm.git

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index a12a246aa..e87795900 100644
--- 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.