aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/discharge.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/discharge.ml')
-rw-r--r--vernac/discharge.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/discharge.ml b/vernac/discharge.ml
index b898f3e83..65ade7887 100644
--- a/vernac/discharge.ml
+++ b/vernac/discharge.ml
@@ -23,7 +23,7 @@ let detype_param =
function
| LocalAssum (Name id, p) -> id, LocalAssumEntry p
| LocalDef (Name id, p,_) -> id, LocalDefEntry p
- | _ -> anomaly (Pp.str "Unnamed inductive local variable")
+ | _ -> anomaly (Pp.str "Unnamed inductive local variable.")
(* Replace