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/."

11 files changed, 15 insertions, 15 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 48fceae9e..36d469e04 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -510,7 +510,7 @@ let raw_map f d =
     let () = match info.evar_body, ans.evar_body with
     | Evar_defined _, Evar_empty
     | Evar_empty, Evar_defined _ ->
-      anomaly (str "Unrespectful mapping function.")
+      anomaly (str "Unrespectful mapping function")
     | _ -> ()
     in
     ans
@@ -524,7 +524,7 @@ let raw_map_undefined f d =
     let ans = f evk info in
     let () = match ans.evar_body with
     | Evar_defined _ ->
-      anomaly (str "Unrespectful mapping function.")
+      anomaly (str "Unrespectful mapping function")
     | _ -> ()
     in
     ans
diff --git a/library/declare.ml b/library/declare.ml
index 95b3674c3..29aa08e77 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"))
diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml
index e3c2b4ad5..2d2dcd0c0 100644
--- a/plugins/ltac/tacenv.ml
+++ b/plugins/ltac/tacenv.ml
@@ -55,7 +55,7 @@ let register_ml_tactic ?(overwrite = false) s (t : ml_tactic array) =
       if overwrite then
         tac_tab := MLTacMap.remove s !tac_tab
       else
-        CErrors.anomaly (str "Cannot redeclare tactic " ++ pr_tacname s ++ str ".")
+        CErrors.anomaly (str "Cannot redeclare tactic " ++ pr_tacname s)
   in
   tac_tab := MLTacMap.add s t !tac_tab
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 6f099c8df..13e2e5d71 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -508,7 +508,7 @@ let rec detype flags avoid env sigma t = CAst.make @@
 	      let body' = EConstr.of_constr body' in
 		substl (c :: List.rev args) body'
 	    with Retyping.RetypeError _ | Not_found -> 
-	      anomaly (str"Cannot detype an unfolded primitive projection.")
+	      anomaly (str"Cannot detype an unfolded primitive projection")
 	  in (detype flags avoid env sigma c').CAst.v
 	else
 	  if print_primproj_params () then
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 630f80ad2..e2106dab5 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -605,7 +605,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
                   postpone to see if other equations help, as in:
                   [Check fun a b c : unit => (eqᵣefl : _ a b = _ c a b)] *)
                UnifFailure (i,NotSameArgSize)
-          | _, _ -> anomaly (Pp.str "Unexpected result from ise_stack2.")
+          | _, _ -> anomaly (Pp.str "Unexpected result from ise_stack2")
 
 	and f2 i =
           if Evar.equal sp1 sp2 then
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index afaa20b6f..10d9173f1 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -183,7 +183,7 @@ let rec nf_val env sigma v typ =
 	try decompose_prod env typ
 	with DestKO ->
           CErrors.anomaly
-            (Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
+            (Pp.strbrk "Returned a functional value in a type not recognized as a product type")
       in
       let env = push_rel (LocalAssum (name,dom)) env in
       let body = nf_val env sigma (f (mk_rel_accu lvl)) codom in
@@ -229,7 +229,7 @@ and nf_args env sigma accu t =
       try decompose_prod env t with
 	DestKO ->
 	CErrors.anomaly
-	  (Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
+	  (Pp.strbrk "Returned a functional value in a type not recognized as a product type")
     in
     let c = nf_val env sigma arg dom in
     (subst1 c codom, c::l)
@@ -246,7 +246,7 @@ and nf_bargs env sigma b t =
 	try decompose_prod env !t with
 	  DestKO ->
 	  CErrors.anomaly
-	    (Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
+	    (Pp.strbrk "Returned a functional value in a type not recognized as a product type")
       in
       let c = nf_val env sigma (block_field b i) dom in
       t := subst1 c codom; c)
@@ -357,7 +357,7 @@ and  nf_predicate env sigma ind mip params v pT =
 	try decompose_prod env pT with
 	  DestKO ->
 	  CErrors.anomaly
-	    (Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
+	    (Pp.strbrk "Returned a functional value in a type not recognized as a product type")
       in
       let dep,body = 
 	nf_predicate (push_rel (LocalAssum (name,dom)) env) sigma ind mip params vb codom in
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index b08666483..ec52da07c 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -314,7 +314,7 @@ and nf_fun env sigma f typ =
     with DestKO ->
       (* 27/2/13: Turned this into an anomaly *)
       CErrors.anomaly
-        (Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
+        (Pp.strbrk "Returned a functional value in a type not recognized as a product type")
   in
   let body = nf_val (push_rel (LocalAssum (name,dom)) env) sigma vb codom in
   mkLambda(name,dom,body)
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 60511d913..e4eb93dd9 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -345,7 +345,7 @@ let tag_var = tag Tag.variable
             hov 1 (str "`" ++ (surround_impl b'
                                  (pr_lident (loc,id) ++ str " : " ++
                                     (if t' then str "!" else mt()) ++ pr t)))
-          |_ -> anomaly (Pp.str "List of generalized binders have alwais one element.")
+          |_ -> anomaly (Pp.str "List of generalized binders have alwais one element")
         end
       | Default b ->
         match t with
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index aaceb7b76..29939294f 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -50,7 +50,7 @@ let cook_this_proof p =
   match p with
   | { Proof_global.id;entries=[constr];persistence;universes } ->
       (id,(constr,universes,persistence))
-  | _ -> CErrors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term.")
+  | _ -> CErrors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term")
 
 let cook_proof () =
   cook_this_proof (fst
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index d6ae0ea86..045eed3e1 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 47ac16f9c..b0b35aed5 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