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/."
---
 vernac/lemmas.ml      | 2 +-
 vernac/obligations.ml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'vernac')

diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index d6ae0ea86f..045eed3e19 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -169,7 +169,7 @@ let look_for_possibly_mutual_statements = function
     let recguard,ordered_inds = find_mutually_recursive_statements thms in
     let thms = List.map pi2 ordered_inds in
     Some recguard,thms, Some (List.map (fun (_,_,i) -> succ i) ordered_inds)
-  | [] -> anomaly (Pp.str "Empty list of theorems.")
+  | [] -> anomaly (Pp.str "Empty list of theorems")
 
 (* Saving a goal *)
 
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 47ac16f9c7..b0b35aed50 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -1166,7 +1166,7 @@ let next_obligation n tac =
   let is_open _ x = Option.is_empty x.obl_body && List.is_empty (deps_remaining obls x.obl_deps) in
   let i = match Array.findi is_open obls with
   | Some i -> i
-  | None -> anomaly (Pp.str "Could not find a solvable obligation.")
+  | None -> anomaly (Pp.str "Could not find a solvable obligation")
   in
   solve_obligation prg i tac
 
-- 
cgit v1.2.3