diff options
Diffstat (limited to 'tactics/tacticals.ml')
| -rw-r--r-- | tactics/tacticals.ml | 11 |
1 files changed, 3 insertions, 8 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 926578e0e..967b6d544 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -475,14 +475,9 @@ module New = struct List.nth hyps (m-1) with Failure _ -> Errors.error "No such assumption." - let nLastDecls n tac = - Proofview.Goal.enter begin fun gl -> - let hyps = - try List.firstn n (Proofview.Goal.hyps gl) - with Failure _ -> error "Not enough hypotheses in the goal." - in - tac hyps - end + let nLastDecls gl n = + try List.firstn n (Proofview.Goal.hyps gl) + with Failure _ -> error "Not enough hypotheses in the goal." let nthHypId m gl = (** We only use [id] *) |