diff options
Diffstat (limited to 'contrib/first-order/instances.ml')
| -rw-r--r-- | contrib/first-order/instances.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/first-order/instances.ml b/contrib/first-order/instances.ml index 423df2f3c7..996ccc0cb7 100644 --- a/contrib/first-order/instances.ml +++ b/contrib/first-order/instances.ml @@ -180,7 +180,7 @@ let right_instance_tac inst continue seq= (fun gls-> split (Rawterm.ImplicitBindings [mkVar (Tacmach.pf_nth_hyp_id gls 1)]) gls); - tclSOLVE [wrap 0 false continue (deepen seq)]]; + tclSOLVE [wrap 0 true continue (deepen seq)]]; tclTRY assumption] | Real ((0,t),_) -> (tclTHEN (split (Rawterm.ImplicitBindings [t])) |