diff options
author | 2017-06-06 00:24:57 +0200 | |
---|---|---|
committer | 2017-06-06 00:24:57 +0200 | |
commit | cc0f9d254c394db742473299336fb20b82ae4aa1 (patch) | |
tree | cbc89906c862624d4285f367d1fa9f0f61f16f05 /vernac/discharge.ml | |
parent | b377bd30f23f430882902f534eaf31b1314ecd07 (diff) | |
parent | 88fdd28815747520bdc555a2d1b8600e114ab341 (diff) |
Merge PR#716: Don't double up on periods in anomalies
Diffstat (limited to 'vernac/discharge.ml')
-rw-r--r-- | vernac/discharge.ml | 2 |
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 |