aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/pfedit.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/pfedit.ml')
-rw-r--r--proofs/pfedit.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index f7d9446b5..ab80841d8 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -126,7 +126,7 @@ let solve_nth ?(with_end_tac=false) gi tac =
Proof_global.run_tactic (Proofview.tclFOCUS gi gi tac)
with
| Proof_global.NoCurrentProof -> Errors.error "No focused proof"
- | Proofview.IndexOutOfRange | Failure "list_chop" ->
+ | Proofview.IndexOutOfRange | Failure "List.chop" ->
let msg = str "No such goal: " ++ int gi ++ str "." in
Errors.errorlabstrm "" msg