diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-12-02 18:29:30 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-12-02 18:48:40 +0100 |
| commit | 801c1c288e1a82a6eeacf7518b2a2a53f4d09c75 (patch) | |
| tree | 29c24000eebff877eebd4da2ecc20efe52f507c2 | |
| parent | ae9f7011a8441a3e34c9fc98497c0e663fb877ca (diff) | |
For compatibility purpose, when setoid_rewriting a hypothesis, beta-iota
normalize it afterwards.
| -rw-r--r-- | tactics/rewrite.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 6523903bd..1245e7c29 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1529,6 +1529,10 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause = in let beta_red _ sigma c = Reductionops.nf_betaiota sigma c in let beta = Proofview.V82.tactic (Tactics.reduct_in_concl (beta_red, DEFAULTcast)) in + let opt_beta = match clause with + | None -> Proofview.tclUNIT () + | Some id -> Proofview.V82.tactic (Tactics.reduct_in_hyp beta_red (id, InHyp)) + in Proofview.Goal.nf_enter begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in @@ -1545,7 +1549,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause = let sigma = match origsigma with None -> sigma | Some sigma -> sigma in treat sigma (res, is_hyp) <*> (** For compatibility *) - beta <*> Proofview.shelve_unifiable + beta <*> opt_beta <*> Proofview.shelve_unifiable with | PretypeError (env, evd, (UnsatisfiableConstraints _ as e)) -> raise (RewriteFailure (Himsg.explain_pretype_error env evd e)) |