X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=493d409da7fb954bfe79811ce53b282f66d9de7e;hb=bdfe00cdb41263098c747853ae6b10fac73fcd35;hp=5828bdea172b52e70743590f62d2662a83a8bc1c;hpb=fa284649ccbac07d9f7c5d6bd329c8ad38f2b93e;p=helm.git

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index 5828bdea1..493d409da 100644
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -882,7 +882,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
       else
         let status = status#set_ng_mode `ProofMode in
         let metasenv,subst,status,indty =
-          GrafiteDisambiguate.disambiguate_nterm status `XTSort [] [] [] (text,prefix_len,indty) in
+          GrafiteDisambiguate.disambiguate_nterm status `XTNone [] [] [] (text,prefix_len,indty) in
         let indtyno, (_,_,tys,_,_),leftno = match indty with
             NCic.Const ((NReference.Ref (_,NReference.Ind (_,indtyno,leftno))) as r) ->
               indtyno, NCicEnvironment.get_checked_indtys status r, leftno