diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 7 | ||||
| -rw-r--r-- | proofs/clenvtac.ml | 1 |
2 files changed, 7 insertions, 1 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 35552b8d85..8c05499a2f 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -356,7 +356,12 @@ let connect_clenv gls clenv = In particular, it assumes that [env'] and [sigma'] extend [env] and [sigma]. *) -let clenv_fchain ?(flags=elim_flags) mv clenv nextclenv = + +let fchain_flags = + { default_unify_flags with + allow_K_in_toplevel_higher_order_unification = true } + +let clenv_fchain ?(flags=fchain_flags) mv clenv nextclenv = (* Add the metavars of [nextclenv] to [clenv], with their name-environment *) let clenv' = { templval = clenv.templval; diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index dad4b5041e..a266405f7a 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -108,6 +108,7 @@ let fail_quick_unif_flags = { resolve_evars = false; use_evars_pattern_unification = false; frozen_evars = ExistentialSet.empty; + restrict_conv_on_strict_subterms = false; (* ? *) modulo_betaiota = false; modulo_eta = true; allow_K_in_toplevel_higher_order_unification = false |