- | (C.Meta (n1,l1), C.Meta (n2,l2)) ->
- n1 = n2 &&
- List.fold_left2
- (fun b t1 t2 ->
- b &&
- match t1,t2 with
- None,_
- | _,None -> true
- | Some t1',Some t2' -> aux test_equality_only context t1' t2'
- ) true l1 l2
- (* TASSI: CONSTRAINTS *)
+ else
+ false,ugraph
+ | (C.Meta (n1,l1), C.Meta (n2,l2)) ->
+ if n1 = n2 then
+ let b2, ugraph1 =
+ let l1 = CicUtil.clean_up_local_context subst metasenv n1 l1 in
+ let l2 = CicUtil.clean_up_local_context subst metasenv n2 l2 in
+ List.fold_left2
+ (fun (b,ugraph) t1 t2 ->
+ if b then
+ match t1,t2 with
+ None,_
+ | _,None -> true,ugraph
+ | Some t1',Some t2' ->
+ aux test_equality_only context t1' t2' ugraph
+ else
+ false,ugraph
+ ) (true,ugraph) l1 l2
+ in
+ if b2 then true,ugraph1 else false,ugraph
+ else
+ false,ugraph
+ (* TASSI: CONSTRAINTS *)