diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-16 20:57:34 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-16 21:17:25 +0200 |
| commit | 9ae9ac00b6882a9918eea3cb7d809424695d37ff (patch) | |
| tree | ee44e2e88516143ce366e7b4ec4be3acc96bc8b1 /plugins/firstorder | |
| parent | 12f4c8ed277fa8368cab2e99f173339a64bcef3d (diff) | |
Put the "exact" family of tactic in the monad.
Diffstat (limited to 'plugins/firstorder')
| -rw-r--r-- | plugins/firstorder/rules.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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; |