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

4 files changed, 7 insertions, 7 deletions

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)