diff options
Diffstat (limited to 'contrib/first-order')
| -rw-r--r-- | contrib/first-order/instances.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/first-order/instances.ml b/contrib/first-order/instances.ml index fac39df93..8eeb8b642 100644 --- a/contrib/first-order/instances.ml +++ b/contrib/first-order/instances.ml @@ -182,11 +182,11 @@ let right_instance_tac inst continue seq= [introf; (fun gls-> split (Rawterm.ImplicitBindings - [inj_open (mkVar (Tacmach.pf_nth_hyp_id gls 1))]) gls); + [mkVar (Tacmach.pf_nth_hyp_id gls 1)]) gls); tclSOLVE [wrap 0 true continue (deepen seq)]]; tclTRY assumption] | Real ((0,t),_) -> - (tclTHEN (split (Rawterm.ImplicitBindings [inj_open t])) + (tclTHEN (split (Rawterm.ImplicitBindings [t])) (tclSOLVE [wrap 0 true continue (deepen seq)])) | Real ((m,t),_) -> tclFAIL 0 (Pp.str "not implemented ... yet") |