) true fl fl'
with
Invalid_argument _ -> false)
- | _,_ -> false (* we already know that t != t' *)
+ | C.Meta (i, subst), C.Meta (i', subst') ->
+ i = i' &&
+ (try
+ List.fold_left2
+ (fun b xt xt' -> match xt,xt' with
+ | Some t, Some t' -> b && aux t t'
+ | _ -> b
+ ) true subst subst'
+ with
+ Invalid_argument _ -> false)
+(* FG: are we _really_ sure of these?
+ | C.Sort (C.Type u), C.Sort (C.Type u') -> u = u'
+ | C.Implicit a, C.Implicit a' -> a = a'
+ we insert an unused variable below to genarate a warning at compile time
+*)
+ | _,_ -> let fix_alpha_equivalence_please = 0 in false (* we already know that t != t' *)
and aux_exp_named_subst exp_named_subst1 exp_named_subst2 =
try
List.fold_left2