- let _,m,p,ty = i.GrafiteTypes.proof in
- Cic.CurrentProof ("current (incomplete) proof",m,p,ty,[],[])
- | Proof (_,m,p,ty) ->
- Cic.CurrentProof ("current proof",m,p,ty,[],[])
+ let _,m,_subst,p,ty, attrs = i.GrafiteTypes.proof in
+ Cic.CurrentProof ("current (incomplete) proof",m,Lazy.force p,ty,[],attrs)
+ | Proof (_,m,_subst,p,ty, attrs) ->
+ Cic.CurrentProof ("current proof",m,Lazy.force p,ty,[],attrs)