aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/tacinterp.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index e5719da990..a12c09ec8c 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1243,7 +1243,7 @@ let solve_remaining_evars env initial_sigma evars c =
Pretype_errors.error_unsolvable_implicit loc env sigma src)
| _ -> map_constr proc_rec c
in
- map_constr proc_rec c
+ proc_rec c
let interp_gen kind ist sigma env (c,ce) =
let (ltacvars,unbndltacvars) = constr_list ist env in