aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/pfedit.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index aaceb7b762..29939294f6 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -50,7 +50,7 @@ let cook_this_proof p =
match p with
| { Proof_global.id;entries=[constr];persistence;universes } ->
(id,(constr,universes,persistence))
- | _ -> CErrors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term.")
+ | _ -> CErrors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term")
let cook_proof () =
cook_this_proof (fst