X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matitaB%2Fcomponents%2Fng_tactics%2FnTacStatus.ml;h=9a6358baaf3e98ee5d4de13bd12e3ee9c02e2e61;hb=6d4277977478ef9bcadaffbef3d4bb04ac0250a5;hp=dc534b43058c04a69125cd6fdf87e4d5630512e2;hpb=98f0fac6d03367be776303e7ba353b75878aaa40;p=helm.git diff --git a/matitaB/components/ng_tactics/nTacStatus.ml b/matitaB/components/ng_tactics/nTacStatus.ml index dc534b430..9a6358baa 100644 --- a/matitaB/components/ng_tactics/nTacStatus.ml +++ b/matitaB/components/ng_tactics/nTacStatus.ml @@ -189,7 +189,7 @@ let disambiguate status context t ty = let status, (_,x) = relocate status context ty in status, Some x in let uri,height,metasenv,subst,obj = status#obj in - let newast, metasenv, subst, status, t = + let metasenv, subst, status, t = GrafiteDisambiguate.disambiguate_nterm status expty context metasenv subst t in let new_pstatus = uri,height,metasenv,subst,obj in