diff options
Diffstat (limited to 'pretyping/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 4f6741d87..003b57693 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1167,7 +1167,7 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t = List.exists (fun op -> eq_constr op cl) l then error_non_linear_unification env evd hdmeta cl else (evd',cl::l) - else if flags.allow_K_in_toplevel_higher_order_unification or dependent op t + else if flags.allow_K_in_toplevel_higher_order_unification || dependent op t then (evd,op::l) else |