diff options
| author | Pierre-Marie Pédrot | 2020-04-30 23:37:15 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-03 13:09:50 +0200 |
| commit | db6fc85ed67e2db7be5d5b8b2dbdbfb37655a5ec (patch) | |
| tree | 243da4cfe886304bb88a35d6bbd8d17e94b7a012 /plugins/ssr/ssrelim.ml | |
| parent | c1b1afe76e1655cc3275bdf4215f0ab690efc3cc (diff) | |
Further port of the SSR tactics.
Diffstat (limited to 'plugins/ssr/ssrelim.ml')
| -rw-r--r-- | plugins/ssr/ssrelim.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index b3fa1ea9d0..6155f8fbf6 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -519,8 +519,8 @@ let perform_injection c = let cl1 = EConstr.mkLambda EConstr.(make_annot Anonymous Sorts.Relevant, mkArrow eqt Sorts.Relevant cl, mkApp (mkRel 1, [|c_eq|])) in let id = injecteq_id in let id_with_ebind = (EConstr.mkVar id, NoBindings) in - let injtac = Tacticals.tclTHEN (introid id) (injectidl2rtac id id_with_ebind) in - Tacticals.tclTHENLAST (Proofview.V82.of_tactic (Tactics.apply (EConstr.compose_lam dc cl1))) injtac gl + let injtac = Tacticals.New.tclTHEN (introid id) (Proofview.V82.tactic (injectidl2rtac id id_with_ebind)) in + Proofview.V82.of_tactic (Tacticals.New.tclTHENLAST (Tactics.apply (EConstr.compose_lam dc cl1)) injtac) gl end let ssrscase_or_inj_tac c = |