aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac/pptactic.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac/pptactic.ml')
-rw-r--r--plugins/ltac/pptactic.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 580c21d40..d66298344 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -582,7 +582,7 @@ type 'a extra_genarg_printer =
hv 0
(pr_let_clause (if recflag then "let rec" else "let") pr hd ++
prlist (fun t -> spc () ++ pr_let_clause "with" pr t) tl)
- | [] -> anomaly (Pp.str "LetIn must declare at least one binding")
+ | [] -> anomaly (Pp.str "LetIn must declare at least one binding.")
let pr_seq_body pr tl =
hv 0 (str "[ " ++