Merge PR#716: Don't double up on periods in anomalies

6 files changed, 14 insertions, 14 deletions

diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index bcd31cb7e..507ff10ee 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -632,7 +632,7 @@ let fix_r2l_forward_rew_scheme (c, ctx') =
 		(EConstr.of_constr (applist (c,
 	          Context.Rel.to_extended_list mkRel 3 indargs @ [mkRel 1;mkRel 3;mkRel 2]))))))))
       in c', ctx'
-  | _ -> anomaly (Pp.str "Ill-formed non-dependent left-to-right rewriting scheme")
+  | _ -> anomaly (Pp.str "Ill-formed non-dependent left-to-right rewriting scheme.")
 
 (**********************************************************************)
 (* Build the right-to-left rewriting lemma for conclusion associated  *)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 268daf6b6..d64cc38ef 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1211,7 +1211,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
     else
       let (a,p_i_minus_1) = match whd_beta_stack !evdref p_i with
 	| (_sigS,[a;p]) -> (a, p)
- 	| _ -> anomaly ~label:"sig_clausal_form" (Pp.str "should be a sigma type") in
+ 	| _ -> anomaly ~label:"sig_clausal_form" (Pp.str "should be a sigma type.") in
       let ev = Evarutil.e_new_evar env evdref a in
       let rty = beta_applist sigma (p_i_minus_1,[ev]) in
       let tuple_tail = sigrec_clausal_form (siglen-1) rty in
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 48a7b3f75..70e62eaba 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -912,7 +912,7 @@ let make_resolve_hyp env sigma decl =
        (c, NamedDecl.get_type decl, Univ.ContextSet.empty)]
   with
     | Failure _ -> []
-    | e when Logic.catchable_exception e -> anomaly (Pp.str "make_resolve_hyp")
+    | e when Logic.catchable_exception e -> anomaly (Pp.str "make_resolve_hyp.")
 
 (* REM : in most cases hintname = id *)
 
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index d15a0724d..4db744224 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -340,7 +340,7 @@ let match_arrow_pattern sigma t =
   match Id.Map.bindings result with
     | [(m1,arg);(m2,mind)] ->
       assert (Id.equal m1 meta1 && Id.equal m2 meta2); (arg, mind)
-    | _ -> anomaly (Pp.str "Incorrect pattern matching")
+    | _ -> anomaly (Pp.str "Incorrect pattern matching.")
 
 let match_with_imp_term sigma c =
   match EConstr.kind sigma c with
@@ -471,7 +471,7 @@ let match_eq_nf gls eqn (ref, hetero) =
     | [(m1,t);(m2,x);(m3,y)] ->
         assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3);
 	(t,pf_whd_all gls x,pf_whd_all gls y)
-    | _ -> anomaly ~label:"match_eq" (Pp.str "an eq pattern should match 3 terms")
+    | _ -> anomaly ~label:"match_eq" (Pp.str "an eq pattern should match 3 terms.")
 
 let dest_nf_eq gls eqn =
   try
@@ -499,7 +499,7 @@ let coq_sig_pattern =
 let match_sigma sigma t =
   match Id.Map.bindings (matches sigma (Lazy.force coq_sig_pattern) t) with
     | [(_,a); (_,p)] -> (a,p)
-    | _ -> anomaly (Pp.str "Unexpected pattern")
+    | _ -> anomaly (Pp.str "Unexpected pattern.")
 
 let is_matching_sigma sigma t = is_matching sigma (Lazy.force coq_sig_pattern) t
 
@@ -545,7 +545,7 @@ let match_eqdec sigma t =
   match Id.Map.bindings subst with
   | [(_,typ);(_,c1);(_,c2)] ->
       eqonleft, Lazy.force op, c1, c2, typ
-  | _ -> anomaly (Pp.str "Unexpected pattern")
+  | _ -> anomaly (Pp.str "Unexpected pattern.")
 
 (* Patterns "~ ?" and "? -> False" *)
 let coq_not_pattern = lazy (mkPattern (mkGAppRef coq_not_ref [mkGHole]))
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index c495b5ece..a7eadc3c3 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -238,7 +238,7 @@ let compute_constructor_signatures isrec ((_,k as ity),u) =
         end
     | LetIn (_,_,_,c), rest -> false :: analrec c rest
     | _, [] -> []
-    | _ -> anomaly (Pp.str "compute_constructor_signatures")
+    | _ -> anomaly (Pp.str "compute_constructor_signatures.")
   in
   let (mib,mip) = Global.lookup_inductive ity in
   let n = mib.mind_nparams in
@@ -613,7 +613,7 @@ module New = struct
     let indmv =
       match EConstr.kind elimclause.evd (last_arg elimclause.evd elimclause.templval.Evd.rebus) with
       | Meta mv -> mv
-      | _         -> anomaly (str"elimination")
+      | _         -> anomaly (str"elimination.")
     in
     let pmv =
       let p, _ = decompose_app elimclause.evd elimclause.templtyp.Evd.rebus in
@@ -700,7 +700,7 @@ module New = struct
   let make_elim_branch_assumptions ba hyps =
     let assums =
       try List.rev (List.firstn ba.nassums hyps)
-      with Failure _ -> anomaly (Pp.str "make_elim_branch_assumptions") in
+      with Failure _ -> anomaly (Pp.str "make_elim_branch_assumptions.") in
     { ba = ba; assums = assums }
 
   let elim_on_ba tac ba =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2a9928a3a..a93a86d3a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1246,7 +1246,7 @@ let cut c =
 let error_uninstantiated_metas t clenv =
   let t = EConstr.Unsafe.to_constr t in
   let na = meta_name clenv.evd (List.hd (Metaset.elements (metavars_of t))) in
-  let id = match na with Name id -> id | _ -> anomaly (Pp.str "unnamed dependent meta")
+  let id = match na with Name id -> id | _ -> anomaly (Pp.str "unnamed dependent meta.")
   in user_err  (str "Cannot find an instance for " ++ pr_id id ++ str".")
 
 let check_unresolved_evars_of_metas sigma clenv =
@@ -1305,13 +1305,13 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true)
 let last_arg sigma c = match EConstr.kind sigma c with
   | App (f,cl) ->
       Array.last cl
-  | _ -> anomaly (Pp.str "last_arg")
+  | _ -> anomaly (Pp.str "last_arg.")
 
 let nth_arg sigma i c =
   if Int.equal i (-1) then last_arg sigma c else
   match EConstr.kind sigma c with
   | App (f,cl) -> cl.(i)
-  | _ -> anomaly (Pp.str "nth_arg")
+  | _ -> anomaly (Pp.str "nth_arg.")
 
 let index_of_ind_arg sigma t =
   let rec aux i j t = match EConstr.kind sigma t with
@@ -4705,7 +4705,7 @@ let elim_scheme_type elim t =
 	  clenv_unify ~flags:(elim_flags ()) Reduction.CUMUL t
             (clenv_meta_type clause mv) clause in
 	Clenvtac.res_pf clause' ~flags:(elim_flags ()) ~with_evars:false
-    | _ -> anomaly (Pp.str "elim_scheme_type")
+    | _ -> anomaly (Pp.str "elim_scheme_type.")
   end }
 
 let elim_type t =