diff options
Diffstat (limited to 'pretyping/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 8955cc64c..886c4a3aa 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -313,9 +313,6 @@ let elim_no_delta_flags = { allow_K_in_toplevel_higher_order_unification = true } -let set_no_head_reduction flags = - { flags with restrict_conv_on_strict_subterms = true } - let use_evars_pattern_unification flags = !global_evars_pattern_unification_flag && flags.use_pattern_unification && Flags.version_strictly_greater Flags.V8_2 |