diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenvtac.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index c966e876f9..22dcca2890 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -96,10 +96,9 @@ let e_res_pf clenv = res_pf clenv ~with_evars:true ~allow_K:false ~flags:dft open Unification let fail_quick_unif_flags = { - modulo_conv_on_closed_terms = true; + modulo_conv_on_closed_terms = Some full_transparent_state; use_metas_eagerly = false; - modulo_delta = Cpred.empty; - modulo_zeta = true; + modulo_delta = empty_transparent_state; } (* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *) |