aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/assumptions.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/assumptions.ml')
-rw-r--r--vernac/assumptions.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index bf274901b..726115653 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -131,7 +131,7 @@ let lookup_constant_in_impl cst fallback =
- The label has not been found in the structure. This is an error *)
match fallback with
| Some cb -> cb
- | None -> anomaly (str "Print Assumption: unknown constant " ++ pr_con cst)
+ | None -> anomaly (str "Print Assumption: unknown constant " ++ pr_con cst ++ str ".")
let lookup_constant cst =
try
@@ -146,7 +146,7 @@ let lookup_mind_in_impl mind =
let fields = memoize_fields_of_mp mp in
search_mind_label lab fields
with Not_found ->
- anomaly (str "Print Assumption: unknown inductive " ++ MutInd.print mind)
+ anomaly (str "Print Assumption: unknown inductive " ++ MutInd.print mind ++ str ".")
let lookup_mind mind =
try Global.lookup_mind mind