From 42d510ceea82d617ac4e630049d690acbe900688 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 31 May 2017 00:49:36 -0400
Subject: Don't double up on periods in anomalies

We don't want "Anomaly: Returned a functional value in a type not
recognized as a product type.. Please report at
http://coq.inria.fr/bugs/." but instead "Anomaly: Returned a functional
value in a type not recognized as a product type. Please report at
http://coq.inria.fr/bugs/."
---
 library/declare.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library')

diff --git a/library/declare.ml b/library/declare.ml
index 95b3674c3e..29aa08e77d 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -415,7 +415,7 @@ let fixpoint_message indexes l =
 
 let cofixpoint_message l =
   Flags.if_verbose Feedback.msg_info (match l with
-  | [] -> anomaly (Pp.str "No corecursive definition.")
+  | [] -> anomaly (Pp.str "No corecursive definition")
   | [id] -> pr_id id ++ str " is corecursively defined"
   | l -> hov 0 (prlist_with_sep pr_comma pr_id l ++
                     spc () ++ str "are corecursively defined"))
-- 
cgit v1.2.3