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

8 files changed, 32 insertions, 32 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 0041797de..c2f705898 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -397,7 +397,7 @@ let rewrite_until_var arg_num eq_ids : tactic =
     then tclIDTAC g
     else
       match eq_ids with
-	| [] -> anomaly (Pp.str "Cannot find a way to prove recursive property");
+	| [] -> anomaly (Pp.str "Cannot find a way to prove recursive property.");
 	| eq_id::eq_ids ->
 	    tclTHEN
 	      (tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (mkVar eq_id))))
@@ -605,7 +605,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
 		   observe (str "cannot compute new term value : " ++ pr_gls g' ++ fnl () ++ str "last hyp is" ++
 			      pr_leconstr_env (pf_env g') (project g') new_term_value_eq
 			   );
-		   anomaly (Pp.str "cannot compute new term value")
+		   anomaly (Pp.str "cannot compute new term value.")
 	   in
 	 let fun_body =
 	   mkLambda(Anonymous,
@@ -838,7 +838,7 @@ let build_proof
 		 h_reduce_with_zeta Locusops.onConcl;
 		 build_proof do_finalize new_infos
 		] g
-	  | Rel _ -> anomaly (Pp.str "Free var in goal conclusion !")
+	  | Rel _ -> anomaly (Pp.str "Free var in goal conclusion!")
   and build_proof do_finalize dyn_infos g =
 (*     observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *)
     observe_tac_stream (str "build_proof with " ++ Printer.pr_leconstr dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g
@@ -1032,7 +1032,7 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a
 		{finfos with
 		   equation_lemma = Some (match Nametab.locate (qualid_of_ident equation_lemma_id) with
 					      ConstRef c -> c
-					    | _ -> CErrors.anomaly (Pp.str "Not a constant")
+					    | _ -> CErrors.anomaly (Pp.str "Not a constant.")
 					 )
 		}
 	  | _ -> ()
@@ -1255,7 +1255,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 	try
 	  let pte =
             try destVar (project gl) pte
-            with DestKO -> anomaly (Pp.str "Property is not a variable")
+            with DestKO -> anomaly (Pp.str "Property is not a variable.")
           in
 	  let fix_info = Id.Map.find  pte ptes_to_fix in
 	  let nb_args = fix_info.nb_realargs in
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 942527167..a0eb9e2b2 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -44,7 +44,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 	   let id = Namegen.next_ident_away x avoid in
 	   Hashtbl.add tbl id x;
 	   RelDecl.set_name (Name id) decl :: change_predicates_names (id::avoid) predicates
-	| Anonymous -> anomaly (Pp.str "Anonymous property binder "))
+	| Anonymous -> anomaly (Pp.str "Anonymous property binder."))
   in
   let avoid = (Termops.ids_of_context env_with_params ) in
   let princ_type_info =
@@ -399,7 +399,7 @@ let get_funs_constant mp dp =
 		     let const = make_con mp dp (Label.of_id id) in
 		     const,i
 		 | Anonymous ->
-		     anomaly (Pp.str "Anonymous fix")
+		     anomaly (Pp.str "Anonymous fix.")
 	    )
 	    na
       | _ -> [|const,0|]
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 8c0b28ae8..785633e25 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1115,7 +1115,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		  new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude)
 		else
 		  CAst.make @@ GProd(n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
-	    | _ -> anomaly (Pp.str "Should not have an anonymous function here")
+	    | _ -> anomaly (Pp.str "Should not have an anonymous function here.")
 		(* We have renamed all the anonymous functions during alpha_renaming phase *)
 
 	end
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 416e196e8..6fd496f50 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -532,7 +532,7 @@ let rec are_unifiable_aux  = function
 	     else
 	       let eqs' =
 		 try (List.combine cpl1 cpl2) @ eqs
-		 with Invalid_argument _ -> anomaly (Pp.str "are_unifiable_aux")
+		 with Invalid_argument _ -> anomaly (Pp.str "are_unifiable_aux.")
 	       in
 	       are_unifiable_aux eqs'
 
@@ -555,7 +555,7 @@ let rec eq_cases_pattern_aux  = function
 	     else
 	       let eqs' =
 		 try (List.combine cpl1 cpl2) @ eqs
-		 with Invalid_argument _ -> anomaly (Pp.str "eq_cases_pattern_aux")
+		 with Invalid_argument _ -> anomaly (Pp.str "eq_cases_pattern_aux.")
 	       in
 	       eq_cases_pattern_aux eqs'
 	 | _ -> raise NotUnifiable
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 6581ac15e..a23c51495 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -734,7 +734,7 @@ let rec add_args id new_args = CAst.map (function
 	    CAppExpl((None,r,None),new_args)
 	| _ -> b
       end
-  | CFix  _  | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo")
+  | CFix  _  | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo.")
   | CProdN(nal,b1) ->
         CProdN(List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal,
 	     add_args id new_args  b1)
@@ -782,9 +782,9 @@ let rec add_args id new_args = CAst.map (function
 	    Miscops.map_cast_type (add_args id new_args) b2)
   | CRecord pars ->
       CRecord (List.map (fun (e,o) -> e, add_args id new_args o) pars)
-  | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation")
-  | CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization")
-  | CDelimiters _ -> anomaly ~label:"add_args " (Pp.str "CDelimiters")
+  | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation.")
+  | CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization.")
+  | CDelimiters _ -> anomaly ~label:"add_args " (Pp.str "CDelimiters.")
   )
 exception Stop of  Constrexpr.constr_expr
 
@@ -826,7 +826,7 @@ let rec chop_n_arrow n t =
 	      chop_n_arrow new_n t'
 	    with Stop t -> t
 	  end
-      | _ -> anomaly (Pp.str "Not enough products")
+      | _ -> anomaly (Pp.str "Not enough products.")
 
 
 let rec get_args b t : Constrexpr.local_binder_expr list *
@@ -856,7 +856,7 @@ let make_graph (f_ref:global_reference) =
       | _ -> raise (UserError (None, str "Not a function reference") )
   in
   (match Global.body_of_constant_body c_body with
-     | None -> error "Cannot build a graph over an axiom !"
+     | None -> error "Cannot build a graph over an axiom!"
      | Some body ->
 	 let env = Global.env () in
 	 let sigma = Evd.from_env env in
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 2476478ab..a73425543 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -369,7 +369,7 @@ let in_Function : function_info -> Libobject.obj =
 
 let find_or_none id =
   try Some
-    (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> CErrors.anomaly (Pp.str "Not a constant")
+    (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> CErrors.anomaly (Pp.str "Not a constant.")
     )
   with Not_found -> None
 
@@ -397,7 +397,7 @@ let add_Function is_general f =
   and prop_lemma = find_or_none (Nameops.add_suffix f_id "_ind")
   and graph_ind =
     match Nametab.locate (qualid_of_ident (mk_rel_id f_id))
-    with | IndRef ind -> ind | _ -> CErrors.anomaly (Pp.str "Not an inductive")
+    with | IndRef ind -> ind | _ -> CErrors.anomaly (Pp.str "Not an inductive.")
   in
   let finfos =
     { function_constant = f;
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 71b41117c..bcfa6b931 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -115,7 +115,7 @@ let generate_type evd g_to_f f graph i =
   let ctxt,_ = decompose_prod_assum !evd graph_arity in
   let fun_ctxt,res_type =
     match ctxt with
-      | [] | [_] -> anomaly (Pp.str "Not a valid context")
+      | [] | [_] -> anomaly (Pp.str "Not a valid context.")
       | decl :: fun_ctxt -> fun_ctxt, RelDecl.get_type decl
   in
   let rec args_from_decl i accu = function
@@ -267,7 +267,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
       	  (fun (_,pat) acc ->
       	     match pat with
 	       | IntroNaming (IntroIdentifier id) -> id::acc
-      	       | _ -> anomaly (Pp.str "Not an identifier")
+      	       | _ -> anomaly (Pp.str "Not an identifier.")
       	  )
       	  (List.nth intro_pats (pred i))
       	  []
@@ -376,7 +376,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
       Array.map
 	(fun ((_,(ctxt,concl))) ->
 	   match ctxt with
-	     | [] | [_] | [_;_] -> anomaly (Pp.str "bad context")
+	     | [] | [_] | [_;_] -> anomaly (Pp.str "bad context.")
 	     | hres::res::decl::ctxt ->
 		let res = EConstr.it_mkLambda_or_LetIn
 			    (EConstr.it_mkProd_or_LetIn concl [hres;res])
@@ -683,7 +683,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
       then
 	let eq_lemma =
 	  try Option.get (infos).equation_lemma
-	  with Option.IsNone -> anomaly (Pp.str "Cannot find equation lemma")
+	  with Option.IsNone -> anomaly (Pp.str "Cannot find equation lemma.")
 	in
 	tclTHENSEQ[
 	  tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) ids;
@@ -913,7 +913,7 @@ let revert_graph kn post_tac hid g =
 	    let info =
 	      try find_Function_of_graph ind'
 	      with Not_found -> (* The graphs are mutually recursive but we cannot find one of them !*)
-		anomaly (Pp.str "Cannot retrieve infos about a mutual block")
+		anomaly (Pp.str "Cannot retrieve infos about a mutual block.")
 	    in
 	    (* if we can find a completeness lemma for this function
 	       then we can come back to the functional form. If not, we do nothing
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 62eba9513..e6f199dba 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -76,7 +76,7 @@ let def_of_const t =
 	     | _ -> raise Not_found)
        with Not_found ->
 	 anomaly (str "Cannot find definition of constant " ++
-		    (Id.print (Label.to_id (con_label (fst sp)))))
+		    (Id.print (Label.to_id (con_label (fst sp)))) ++ str ".")
       )
      |_ -> assert false
 
@@ -95,7 +95,7 @@ let constant sl s = constr_of_global (find_reference sl s)
 
 let const_of_ref = function
     ConstRef kn -> kn
-  | _ -> anomaly (Pp.str "ConstRef expected")
+  | _ -> anomaly (Pp.str "ConstRef expected.")
 
 
 let nf_zeta env =
@@ -442,7 +442,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g =
 	travel jinfo new_continuation_tac 
 	  {expr_info with info = b; is_final=false} g
       end
-    | Rel _ -> anomaly (Pp.str "Free var in goal conclusion !")
+    | Rel _ -> anomaly (Pp.str "Free var in goal conclusion!")
     | Prod _ -> 
       begin
 	try
@@ -486,7 +486,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g =
 	    travel_args jinfo
 	      expr_info.is_main_branch new_continuation_tac new_infos g
 	  | Case _ ->  user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)")
-	  | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr expr_info.info)
+	  | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr expr_info.info ++ Pp.str ".")
       end
     | Cast(t,_,_) -> travel jinfo continuation_tac {expr_info with info=t} g
     | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ ->
@@ -1165,7 +1165,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a
       let f_id =
 	match f_name with
 	  | Name f_id -> next_ident_away_in_goal f_id ids
-	  | Anonymous -> anomaly (Pp.str "Anonymous function")
+	  | Anonymous -> anomaly (Pp.str "Anonymous function.")
       in
       let n_names_types,_ = decompose_lam_n sigma nb_args body1 in
       let n_ids,ids =
@@ -1175,7 +1175,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a
 	       | Name id ->
 		   let n_id = next_ident_away_in_goal id ids in
 		   n_id::n_ids,n_id::ids
-	       | _ -> anomaly (Pp.str "anonymous argument")
+	       | _ -> anomaly (Pp.str "anonymous argument.")
 	  )
 	  ([],(f_id::ids))
 	  n_names_types
@@ -1302,7 +1302,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
     | None   ->
 	try add_suffix current_proof_name "_subproof"
 	with e when CErrors.noncritical e ->
-          anomaly (Pp.str "open_new_goal with an unamed theorem")
+          anomaly (Pp.str "open_new_goal with an unamed theorem.")
   in
   let na = next_global_ident_away name [] in
   if Termops.occur_existential sigma gls_type then
@@ -1313,7 +1313,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
       let na_global = Smartlocate.global_with_alias na_ref in
       match na_global with
 	  ConstRef c -> is_opaque_constant c
-	| _ -> anomaly ~label:"equation_lemma" (Pp.str "not a constant")
+	| _ -> anomaly ~label:"equation_lemma" (Pp.str "not a constant.")
     in
     let lemma = mkConst (Names.Constant.make1 (Lib.make_kn na)) in
     ref_ := Value (EConstr.Unsafe.to_constr lemma);
@@ -1464,7 +1464,7 @@ let (com_eqn : int -> Id.t ->
     let opacity =
       match terminate_ref with
 	| ConstRef c -> is_opaque_constant c
-	| _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant")
+	| _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.")
     in
     let (evmap, env) = Lemmas.get_current_context() in
     let evmap = Evd.from_ctx (Evd.evar_universe_context evmap) in