diff options
| author | Erik Martin-Dorel | 2019-03-04 01:25:39 +0100 |
|---|---|---|
| committer | Erik Martin-Dorel | 2019-04-23 20:22:05 +0200 |
| commit | bb6dc2355bcd027a3a89c40629b82eb2019eff6a (patch) | |
| tree | 97495eceee09a17c9739f8e1db532ccde54e203c /plugins/ssr/ssrequality.ml | |
| parent | 7c598f9f1f6da2cecc70557f9f436392322fc6d9 (diff) | |
[ssr] under: Add iff support in side-conditions
Diffstat (limited to 'plugins/ssr/ssrequality.ml')
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index ff6dd8f75a..842e4feecf 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -406,7 +406,7 @@ let rwcltac ?under ?map_redex cl rdx dir sr gl = let cl' = EConstr.mkApp (EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdxt cl, [|rdx|]) in let sigma, _ = Typing.type_of env sigma cl' in let gl = pf_merge_uc_of sigma gl in - Proofview.V82.of_tactic (convert_concl cl'), rewritetac dir r', gl + Proofview.V82.of_tactic (convert_concl cl'), rewritetac ?under dir r', gl else let dc, r2 = EConstr.decompose_lam_n_assum (project gl) n r' in let r3, _, r3t = @@ -417,7 +417,7 @@ let rwcltac ?under ?map_redex cl rdx dir sr gl = let cl'' = EConstr.mkNamedProd (make_annot pattern_id Sorts.Relevant) rdxt cl' in let itacs = [introid pattern_id; introid rule_id] in let cltac = Proofview.V82.of_tactic (Tactics.clear [pattern_id; rule_id]) in - let rwtacs = [rewritetac dir (EConstr.mkVar rule_id); cltac] in + let rwtacs = [rewritetac ?under dir (EConstr.mkVar rule_id); cltac] in apply_type cl'' [rdx; EConstr.it_mkLambda_or_LetIn r3 dc], tclTHENLIST (itacs @ rwtacs), gl in let cvtac' _ = |