diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 16 |
1 files changed, 7 insertions, 9 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index a7fc38a23a..d6083860a9 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -170,9 +170,8 @@ let instantiate_lemma gl c ty l l2r concl = let eqclause = pf_apply Clenv.make_clenv_binding gl (c,t) l in [eqclause] -let rewrite_conv_closed_core_unif_flags env = - let ts = Conv_oracle.get_transp_state (Environ.oracle env) in { - modulo_conv_on_closed_terms = Some ts; +let rewrite_conv_closed_core_unif_flags = { + modulo_conv_on_closed_terms = Some full_transparent_state; (* We have this flag for historical reasons, it has e.g. the consequence *) (* to rewrite "?x+2" in "y+(1+1)=0" or to rewrite "?x+?x" in "2+(1+1)=0" *) @@ -198,18 +197,17 @@ let rewrite_conv_closed_core_unif_flags env = modulo_eta = true; } -let rewrite_conv_closed_unif_flags env = - let flags = rewrite_conv_closed_core_unif_flags env in { - core_unify_flags = flags; - merge_unify_flags = flags; - subterm_unify_flags = flags; +let rewrite_conv_closed_unif_flags = { + core_unify_flags = rewrite_conv_closed_core_unif_flags; + merge_unify_flags = rewrite_conv_closed_core_unif_flags; + subterm_unify_flags = rewrite_conv_closed_core_unif_flags; allow_K_in_toplevel_higher_order_unification = false; resolve_evars = false } let rewrite_elim with_evars frzevars cls c e = Proofview.Goal.enter begin fun gl -> - let flags = make_flags frzevars (Proofview.Goal.sigma gl) (rewrite_conv_closed_unif_flags (Proofview.Goal.env gl)) c in + let flags = make_flags frzevars (Proofview.Goal.sigma gl) rewrite_conv_closed_unif_flags c in general_elim_clause with_evars flags cls c e end |