- let rec aux b = function
- | Cic.Rel n, Cic.Rel m -> if n = m then true else false
- | ((Cic.Appl l) as left),((Cic.Appl l') as right) ->
- check b left right ||
- (try
- List.for_all2 (fun t t' -> aux true (t,t')) (List.tl l) (List.tl l')
- with Invalid_argument _ -> false)
- | (Cic.Meta _),_
- | _,(Cic.Meta _) -> false
- | _ -> false
+ let rec aux b (ok_so_far, subsumption_used) t1 t2 =
+ match t1,t2 with
+ | t1, t2 when not ok_so_far -> ok_so_far, subsumption_used
+ | t1, t2 when subsumption_used -> t1 = t2, subsumption_used
+ | Cic.Appl (h1::l),Cic.Appl (h2::l') when h1 = h2 ->
+ let rc = check_subsumed b t1 t1 in
+ if rc then
+ true, true
+ else
+ (try
+ List.fold_left2
+ (fun (ok_so_far, subsumption_used) t t' ->
+ aux true (ok_so_far, subsumption_used) t t')
+ (ok_so_far, subsumption_used) l l'
+ with Invalid_argument _ -> false,subsumption_used)
+ | _ -> false, subsumption_used