diff options
| -rw-r--r-- | tactics/tacinterp.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 65621a028..3012cbae2 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1570,9 +1570,8 @@ let interp_induction_arg ist gl sigma arg = let env = pf_env gl in match arg with | ElimOnConstr c -> - let sigma', (c,b) = interp_constr_with_bindings ist env sigma c in - let sigma, c = solve_remaining_evars false true env sigma sigma' c in - sigma, ElimOnConstr (c,b) + let sigma, c = interp_constr_with_bindings ist env sigma c in + sigma, ElimOnConstr c | ElimOnAnonHyp n as x -> sigma, x | ElimOnIdent (loc,id) -> try |