used to be the zeta-expanded form. It is now the reference.
| Some (_,C.Def (_,Some ty)) ->
t,S.lift n ty,subst,metasenv, ugraph
| Some (_,C.Def (bo,None)) ->
| Some (_,C.Def (_,Some ty)) ->
t,S.lift n ty,subst,metasenv, ugraph
| Some (_,C.Def (bo,None)) ->
- type_of_aux subst metasenv context (S.lift n bo) ugraph
+ let _,ty,subst,metasenv,ugraph =
+ type_of_aux subst metasenv context (S.lift n bo) ugraph
+ in
+ t,ty,subst,metasenv,ugraph
| None -> raise (RefineFailure "Rel to hidden hypothesis")
with
_ -> raise (RefineFailure "Not a close term")
| None -> raise (RefineFailure "Rel to hidden hypothesis")
with
_ -> raise (RefineFailure "Not a close term")