From a1a6d7b99eef5e6a671e5e6d057e46a6122e5e58 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 23 Nov 2014 12:27:19 +0100 Subject: Experimenting always forcing convertibility on strict implicit arguments in tactic unification. --- tactics/equality.ml | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) (limited to 'tactics') diff --git a/tactics/equality.ml b/tactics/equality.ml index d6083860a9..a7fc38a23a 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -170,8 +170,9 @@ 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 = { - modulo_conv_on_closed_terms = Some full_transparent_state; +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; (* 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" *) @@ -197,17 +198,18 @@ let rewrite_conv_closed_core_unif_flags = { modulo_eta = true; } -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; +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; 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 c in + let flags = make_flags frzevars (Proofview.Goal.sigma gl) (rewrite_conv_closed_unif_flags (Proofview.Goal.env gl)) c in general_elim_clause with_evars flags cls c e end -- cgit v1.2.3