aboutsummaryrefslogtreecommitdiffhomepage
path: root/ltac/tacinterp.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ltac/tacinterp.ml')
-rw-r--r--ltac/tacinterp.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 5aff262aa..7ec1b2ca0 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -1755,7 +1755,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
Tacticals.New.tclWITHHOLES false
(name_atomic ~env
(TacGeneralize cl)
- (Proofview.V82.tactic (Tactics.generalize_gen cl))) sigma
+ (Tactics.generalize_gen cl)) sigma
end }
| TacLetTac (na,c,clp,b,eqpat) ->
Proofview.V82.nf_evar_goals <*>