- | Cic.LetIn (Cic.Anonymous, s1, t1), Cic.LetIn (name, s2, t2) ->
- aux context s1 s2 @ aux (add_ctx context name (Cic.Def (s2,None))) t1 t2
- | Cic.LetIn (Cic.Name n1, s1, t1),
- Cic.LetIn ((Cic.Name n2) as name, s2, t2) when n1 = n2->
- aux context s1 s2 @ aux (add_ctx context name (Cic.Def (s2,None))) t1 t2
- | Cic.LetIn (name1, s1, t1), Cic.LetIn (name2, s2, t2) -> []
+ | Cic.LetIn (Cic.Anonymous, s1, ty1, t1), Cic.LetIn (name, s2, ty2, t2) ->
+ aux context s1 s2 @
+ aux context ty1 ty2 @
+ aux (add_ctx context name (Cic.Def (s2,ty2))) t1 t2
+ | Cic.LetIn (Cic.Name n1, s1, ty1, t1),
+ Cic.LetIn ((Cic.Name n2) as name, s2, ty2, t2) when n1 = n2->
+ aux context s1 s2 @
+ aux context ty1 ty2 @
+ aux (add_ctx context name (Cic.Def (s2,ty2))) t1 t2
+ | Cic.LetIn (name1, s1, ty1, t1), Cic.LetIn (name2, s2, ty2, t2) -> []