diff options
Diffstat (limited to 'plugins/firstorder/instances.ml')
| -rw-r--r-- | plugins/firstorder/instances.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index ac612d0cd..0acdc4c80 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -143,11 +143,11 @@ let left_instance_tac (inst,id) continue seq= else tclTHENS (cut dom) [tclTHENLIST - [introf; + [Proofview.V82.of_tactic introf; (fun gls->generalize [mkApp(constr_of_global id, [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls); - introf; + Proofview.V82.of_tactic introf; tclSOLVE [wrap 1 false continue (deepen (record (id,None) seq))]]; tclTRY assumption] @@ -168,7 +168,7 @@ let left_instance_tac (inst,id) continue seq= in tclTHENLIST [special_generalize; - introf; + Proofview.V82.of_tactic introf; tclSOLVE [wrap 1 false continue (deepen (record (id,Some c) seq))]] @@ -177,14 +177,14 @@ let right_instance_tac inst continue seq= Phantom dom -> tclTHENS (cut dom) [tclTHENLIST - [introf; + [Proofview.V82.of_tactic introf; (fun gls-> - split (ImplicitBindings - [mkVar (Tacmach.pf_nth_hyp_id gls 1)]) gls); + Proofview.V82.of_tactic (split (ImplicitBindings + [mkVar (Tacmach.pf_nth_hyp_id gls 1)])) gls); tclSOLVE [wrap 0 true continue (deepen seq)]]; tclTRY assumption] | Real ((0,t),_) -> - (tclTHEN (split (ImplicitBindings [t])) + (tclTHEN (Proofview.V82.of_tactic (split (ImplicitBindings [t]))) (tclSOLVE [wrap 0 true continue (deepen seq)])) | Real ((m,t),_) -> tclFAIL 0 (Pp.str "not implemented ... yet") |