- n1 = n2 &&
- 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 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 *)
+ 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 *)