- try
- unify rdb test_eq_only metasenv subst context
- (C.Meta (i,l)) lambda_Mj swap
- with UnificationFailure msg | Uncertain msg when not norm2->
- (* failure: let's try again argument vs argument *)
- raise (KeepReducing msg)
+ unify rdb test_eq_only metasenv subst context
+ (C.Meta (i,l)) lambda_Mj swap