- test_equality_only metasenv subst context t2 args in
- fo_unif_subst test_equality_only subst context metasenv
- (C.Meta (i,l)) beta_expanded)
->>>>>>> 1.40
- | _, C.Meta (i,l)::args ->
-<<<<<<< cicUnification.ml
- let subst,metasenv,t1',ugraph1 =
- beta_expand_many test_equality_only metasenv subst context t1 args
- ugraph
- in
- subst,metasenv,t1',t2,ugraph1
-=======
+ test_equality_only metasenv subst context t2 args ugraph
+ in
+ fo_unif_subst test_equality_only subst context metasenv
+ (C.Meta (i,l)) beta_expanded ugraph1)
+ | _, C.Meta (i,l)::args when not(exists_a_meta args) ->