Record projections:

[helm.git] / matitaB / components / ng_tactics / nTacStatus.ml

diff --git a/matitaB/components/ng_tactics/nTacStatus.ml b/matitaB/components/ng_tactics/nTacStatus.ml
index dc534b43058c04a69125cd6fdf87e4d5630512e2..9a6358baaf3e98ee5d4de13bd12e3ee9c02e2e61 100644 (file)
--- 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