From 9ae9ac00b6882a9918eea3cb7d809424695d37ff Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 16 May 2016 20:57:34 +0200 Subject: Put the "exact" family of tactic in the monad. --- plugins/firstorder/rules.ml | 4 ++-- plugins/rtauto/refl_tauto.ml | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) (limited to 'plugins') diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index f19cdd2cc..d05e9484a 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -58,7 +58,7 @@ let clear_global=function (* connection rules *) let axiom_tac t seq= - try pf_constr_of_global (find_left t seq) exact_no_check + try pf_constr_of_global (find_left t seq) (fun c -> Proofview.V82.of_tactic (exact_no_check c)) with Not_found->tclFAIL 0 (Pp.str "No axiom link") let ll_atom_tac a backtrack id continue seq= @@ -151,7 +151,7 @@ let ll_arrow_tac a b c backtrack id continue seq= clear_global id; wrap 1 false continue seq]; tclTHENS (Proofview.V82.of_tactic (cut cc)) - [pf_constr_of_global id exact_no_check; + [pf_constr_of_global id (fun c -> Proofview.V82.of_tactic (exact_no_check c)); tclTHENLIST [pf_constr_of_global id (fun idc -> generalize [d idc]); clear_global id; diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 2f3a3e551..73dc13e72 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -316,7 +316,7 @@ let rtauto_tac gls= if !check then Proofview.V82.of_tactic (Tactics.exact_check term) gls else - Tactics.exact_no_check term gls in + Proofview.V82.of_tactic (Tactics.exact_no_check term) gls in let tac_end_time = System.get_time () in let _ = if !check then msg_info (str "Proof term type-checking is on"); -- cgit v1.2.3