diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacinterp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index cc09170107..7f18065fe6 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -958,7 +958,7 @@ let interp_induction_arg ist gl arg = else let c = (GVar (loc,id),Some (CRef (Ident (loc,id),None))) in let f env sigma = - let (sigma,c) = interp_constr ist env sigma c in + let (sigma,c) = interp_open_constr ist env sigma c in sigma,(c,NoBindings) in keep,ElimOnConstr f |