* Moreover the inferred type is closer to the expected one.
*)
C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty,
- subst',metasenv',ugraph2
+ subst'',metasenv'',ugraph2
| C.Appl (he::((_::_) as tl)) ->
let he',hetype,subst',metasenv',ugraph1 =
type_of_aux subst metasenv context he ugraph
let t = CicSubstitution.subst t' t in
i - 1,t
) tys (typesno - 1,t)) in
- let ty' = undebrujin ty in
+ let ty' = undebrujin ty' in
metasenv,ugraph,(name,ty')::res
) cl (metasenv,ugraph,[])
in