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/ssrtacticals.ml | |
| parent | c1b1afe76e1655cc3275bdf4215f0ab690efc3cc (diff) | |
Further port of the SSR tactics.
Diffstat (limited to 'plugins/ssr/ssrtacticals.ml')
| -rw-r--r-- | plugins/ssr/ssrtacticals.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml index 4f9747ae73..a379b2561a 100644 --- a/plugins/ssr/ssrtacticals.ml +++ b/plugins/ssr/ssrtacticals.ml @@ -132,7 +132,7 @@ let tclCLAUSES tac (gens, clseq) = Proofview.V82.tactic begin fun gl -> if clseq = InGoal || clseq = InSeqGoal then tac gl else let clr_gens = pf_clauseids gl gens clseq in - let clear = Tacticals.tclTHENLIST (List.rev(List.fold_right clr_of_wgen clr_gens [])) in + let clear = Tacticals.New.tclTHENLIST (List.rev(List.fold_right clr_of_wgen clr_gens [])) in let gl_id = mk_anon_id hidden_goal_tag (Tacmach.pf_ids_of_hyps gl) in let cl0 = pf_concl gl in let dtac gl = @@ -145,7 +145,7 @@ let tclCLAUSES tac (gens, clseq) = | _, Some ((x,_),_) -> let id = hoi_id x in Some (mk_discharged_id id, id) | _, None -> None) gens in endclausestac id_map clseq gl_id cl0 in - Tacticals.tclTHENLIST (hidetacs clseq gl_id cl0 @ [dtac; clear; tac; endtac]) gl + Tacticals.tclTHENLIST (hidetacs clseq gl_id cl0 @ [dtac; Proofview.V82.of_tactic clear; tac; endtac]) gl end (** The "do" tactical. ********************************************************) |