- if alpha then
- if NCicReduction.alpha_eq metasenv subst context li t then
- Some ((metasenv,subst), NCic.Rel (i+1+k))
- else
- None
- else
- match unify metasenv subst context li t with
- | Some (metasenv,subst) ->
- Some ((metasenv, subst), NCic.Rel (i+1+k))
- | None -> None)
+ match unify metasenv subst context li t with
+ | Some (metasenv,subst) ->
+ Some ((metasenv, subst), NCic.Rel (i+1+k))
+ | None -> None)