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

15 files changed, 38 insertions, 38 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 80680e4088..efab5b9779 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -70,7 +70,7 @@ let error_wrong_numarg_inductive ?loc env c n =
 
 let list_try_compile f l =
   let rec aux errors = function
-  | [] -> if errors = [] then anomaly (str "try_find_f") else iraise (List.last errors)
+  | [] -> if errors = [] then anomaly (str "try_find_f.") else iraise (List.last errors)
   | h::t ->
       try f h
       with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _ as e ->
@@ -162,9 +162,9 @@ let feed_history arg = function
   | Continuation (n, l, h) when n>=1 ->
       Continuation (n-1, arg :: l, h)
   | Continuation (n, _, _) ->
-      anomaly (str "Bad number of expected remaining patterns: " ++ int n)
+      anomaly (str "Bad number of expected remaining patterns: " ++ int n ++ str ".")
   | Result _ ->
-      anomaly (Pp.str "Exhausted pattern history")
+      anomaly (Pp.str "Exhausted pattern history.")
 
 (* This is for non exhaustive error message *)
 
@@ -190,7 +190,7 @@ let pop_history_pattern = function
   | Continuation (0, l, MakeConstructor (pci, rh)) ->
       feed_history (CAst.make @@ PatCstr (pci,List.rev l,Anonymous)) rh
   | _ ->
-      anomaly (Pp.str "Constructor not yet filled with its arguments")
+      anomaly (Pp.str "Constructor not yet filled with its arguments.")
 
 let pop_history h =
   feed_history (CAst.make @@ PatVar Anonymous) h
@@ -425,7 +425,7 @@ let lift_tomatch_type n = liftn_tomatch_type n 1
 let current_pattern eqn =
   match eqn.patterns with
     | pat::_ -> pat
-    | [] -> anomaly (Pp.str "Empty list of patterns")
+    | [] -> anomaly (Pp.str "Empty list of patterns.")
 
 let alias_of_pat = CAst.with_val (function
   | PatVar name -> name
@@ -438,7 +438,7 @@ let remove_current_pattern eqn =
 	{ eqn with
 	    patterns = pats;
 	    alias_stack = alias_of_pat pat :: eqn.alias_stack }
-    | [] -> anomaly (Pp.str "Empty list of patterns")
+    | [] -> anomaly (Pp.str "Empty list of patterns.")
 
 let push_current_pattern (cur,ty) eqn =
   match eqn.patterns with
@@ -447,7 +447,7 @@ let push_current_pattern (cur,ty) eqn =
 	{ eqn with
             rhs = { eqn.rhs with rhs_env = rhs_env };
 	    patterns = pats }
-    | [] -> anomaly (Pp.str "Empty list of patterns")
+    | [] -> anomaly (Pp.str "Empty list of patterns.")
 
 (* spiwack: like [push_current_pattern] but does not introduce an
    alias in rhs_env. Aliasing binders are only useful for variables at
@@ -457,7 +457,7 @@ let push_noalias_current_pattern eqn =
   match eqn.patterns with
   | _::pats ->
       { eqn with patterns = pats }
-  | [] -> anomaly (Pp.str "push_noalias_current_pattern: Empty list of patterns")
+  | [] -> anomaly (Pp.str "push_noalias_current_pattern: Empty list of patterns.")
 
 
 
@@ -641,7 +641,7 @@ let replace_tomatch sigma n c =
   | Pushed (initial,((b,tm),l,na)) :: rest ->
       let b = replace_term sigma n c depth b in
       let tm = map_tomatch_type (replace_term sigma n c depth) tm in
-      List.iter (fun i -> if Int.equal i (n + depth) then anomaly (Pp.str "replace_tomatch")) l;
+      List.iter (fun i -> if Int.equal i (n + depth) then anomaly (Pp.str "replace_tomatch.")) l;
       Pushed (initial,((b,tm),l,na)) :: replrec depth rest
   | Alias (initial,(na,b,d)) :: rest ->
       (* [b] is out of replacement scope *)
@@ -882,7 +882,7 @@ let specialize_predicate_var (cur,typ,dep) env tms ccl =
 (*****************************************************************************)
 let generalize_predicate sigma (names,na) ny d tms ccl =
   let () = match na with
-  | Anonymous -> anomaly (Pp.str "Undetected dependency")
+  | Anonymous -> anomaly (Pp.str "Undetected dependency.")
   | _ -> () in
   let p = List.length names + 1 in
   let ccl = lift_predicate 1 ccl tms in
@@ -1708,7 +1708,7 @@ let build_tycon ?loc env tycon_env s subst tycon extenv evdref t =
         evdref := evd;
         (t,tt) in
   let b = e_cumul env evdref tt (mkSort s) (* side effect *) in
-  if not b then anomaly (Pp.str "Build_tycon: should be a type");
+  if not b then anomaly (Pp.str "Build_tycon: should be a type.");
   { uj_val = t; uj_type = tt }
 
 (* For a multiple pattern-matching problem Xi on t1..tn with return
@@ -1872,7 +1872,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
 		  if not (eq_ind ind ind') then
 		    user_err ?loc  (str "Wrong inductive type.");
 		  if not (Int.equal nrealargs_ctxt (List.length realnal)) then
-		      anomaly (Pp.str "Ill-formed 'in' clause in cases");
+		      anomaly (Pp.str "Ill-formed 'in' clause in cases.");
 		  List.rev realnal
 	      | None -> List.make nrealargs_ctxt Anonymous in
 	  LocalAssum (na, EConstr.of_constr (build_dependent_inductive env0 indf'))
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 83c26058ac..1282e3cb86 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -67,7 +67,7 @@ let apply_coercion_args env evd check isproj argl funj =
         if check && not (e_cumul env evdref (Retyping.get_type_of env !evdref h) c1) then
 	  raise NoCoercion;
         apply_rec (h::acc) (subst1 h c2) restl
-      | _ -> anomaly (Pp.str "apply_coercion_args")
+      | _ -> anomaly (Pp.str "apply_coercion_args.")
   in
   let res = apply_rec [] funj.uj_type argl in
     !evdref, res
@@ -368,7 +368,7 @@ let apply_coercion env sigma p hj typ_cl =
       (hj,typ_cl,sigma) p
     in evd, j
   with NoCoercion as e -> raise e
-  | e when CErrors.noncritical e -> anomaly (Pp.str "apply_coercion")
+  | e when CErrors.noncritical e -> anomaly (Pp.str "apply_coercion.")
 
 (* Try to coerce to a funclass; raise NoCoercion if not possible *)
 let inh_app_fun_core env evd j =
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 6f099c8dfd..c93b1e568c 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -425,7 +425,7 @@ type binder_kind = BProd | BLambda | BLetIn
 (**********************************************************************)
 (* Main detyping function                                             *)
 
-let detype_anonymous = ref (fun ?loc n -> anomaly ~label:"detype" (Pp.str "index to an anonymous variable"))
+let detype_anonymous = ref (fun ?loc n -> anomaly ~label:"detype" (Pp.str "index to an anonymous variable."))
 let set_detype_anonymous f = detype_anonymous := f
 
 let detype_level sigma l =
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 630f80ad2f..1d6b611da4 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1088,7 +1088,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
       let filter' = filter_possible_projections evd c ty ctxt args in
       (id,t,c,ty,evs,Filter.make filter',occs) :: make_subst (ctxt',l,occsl)
   | _, _, [] -> []
-  | _ -> anomaly (Pp.str "Signature or instance are shorter than the occurrences list") in
+  | _ -> anomaly (Pp.str "Signature or instance are shorter than the occurrences list.") in
 
   let rec set_holes evdref rhs = function
   | (id,_,c,cty,evsref,filter,occs)::subst ->
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 98e71c7fd9..de5a627266 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -634,7 +634,7 @@ let make_projectable_subst aliases sigma evi args =
                    cstrs)
             | _ ->
                 (rest,Id.Map.add id [a,normalize_alias_opt sigma aliases a,id] all,cstrs))
-        | _ -> anomaly (Pp.str "Instance does not match its signature"))
+        | _ -> anomaly (Pp.str "Instance does not match its signature."))
       sign (Array.rev_to_list args,Id.Map.empty,Constrmap.empty) in
   (full_subst,cstr_subst)
 
@@ -828,7 +828,7 @@ let rec find_projectable_vars with_evars aliases sigma y subst =
             | _ -> subst'
           end
         | [] -> subst'
-        | _ -> anomaly (Pp.str "More than one non var in aliases class of evar instance")
+        | _ -> anomaly (Pp.str "More than one non var in aliases class of evar instance.")
       else
         subst' in
   Id.Map.fold is_projectable subst []
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index c4a74d990b..8a902f3a33 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -296,7 +296,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
 	   process_constr (push_rel d env) (i+1) (lift 1 f)
 	     (cprest,rest))
     | [],[] -> f
-    | _,[] | [],_ -> anomaly (Pp.str "process_constr")
+    | _,[] | [],_ -> anomaly (Pp.str "process_constr.")
 
   in
   process_constr env 0 f (List.rev cstr.cs_args, recargs)
@@ -533,7 +533,7 @@ let weaken_sort_scheme env evd set sort npars term ty =
 	    mkProd (n, t, c'), mkLambda (n, t, term')
       | LetIn (n,b,t,c) -> let c',term' = drec np c in
            mkLetIn (n,b,t,c'), mkLetIn (n,b,t,term')
-      | _ -> anomaly ~label:"weaken_sort_scheme" (Pp.str "wrong elimination type")
+      | _ -> anomaly ~label:"weaken_sort_scheme" (Pp.str "wrong elimination type.")
   in
   let ty, term = drec npars ty in
     !evdref, ty, term
@@ -577,7 +577,7 @@ let build_mutual_induction_scheme env sigma = function
       in
       let _ = check_arities env listdepkind in
       mis_make_indrec env sigma listdepkind mib u
-  | _ -> anomaly (Pp.str "build_induction_scheme expects a non empty list of inductive types")
+  | _ -> anomaly (Pp.str "build_induction_scheme expects a non empty list of inductive types.")
 
 let build_induction_scheme env sigma pind dep kind =
   let (mib,mip) = lookup_mind_specif env (fst pind) in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 7f3bafc685..d8252ea9bb 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -538,7 +538,7 @@ let is_predicate_explicitly_dep env sigma pred arsign =
           | Name _ -> true
           end
 
-      | _ -> anomaly (Pp.str "Non eta-expanded dep-expanded \"match\" predicate")
+      | _ -> anomaly (Pp.str "Non eta-expanded dep-expanded \"match\" predicate.")
   in
   srec env (EConstr.of_constr pred) arsign
 
diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml
index 211ffbe01e..e555742bca 100644
--- a/pretyping/locusops.ml
+++ b/pretyping/locusops.ml
@@ -84,7 +84,7 @@ let concrete_clause_of enum_hyps cl =
 (** Miscellaneous functions *)
 
 let out_arg = function
-  | Misctypes.ArgVar _ -> CErrors.anomaly (Pp.str "Unevaluated or_var variable")
+  | Misctypes.ArgVar _ -> CErrors.anomaly (Pp.str "Unevaluated or_var variable.")
   | Misctypes.ArgArg x -> x
 
 let occurrences_of_hyp id cls =
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index afaa20b6f6..61118cf777 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -139,7 +139,7 @@ let type_of_var env id =
   let open Context.Named.Declaration in
   try env |> lookup_named id |> get_type
   with Not_found ->
-    anomaly ~label:"type_of_var" (str "variable " ++ Id.print id ++ str " unbound")
+    anomaly ~label:"type_of_var" (str "variable " ++ Id.print id ++ str " unbound.")
 
 let sort_of_product env domsort rangsort =
   match (domsort, rangsort) with
@@ -405,7 +405,7 @@ let native_norm env sigma c ty =
         let time_info = Format.sprintf "Reification done in %.5f@." (t2 -. t1) in
         if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
         EConstr.of_constr res
-    | _ -> anomaly (Pp.str "Compilation failure") 
+    | _ -> anomaly (Pp.str "Compilation failure.") 
 
 let native_conv_generic pb sigma t =
   Nativeconv.native_conv_gen pb (evars_of_evar_map sigma) t
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 71dbc39f3f..db2e5da957 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -112,14 +112,14 @@ let rec head_pattern_bound t =
 	-> raise BoundPattern
     (* Perhaps they were arguments, but we don't beta-reduce *)
     | PLambda _ -> raise BoundPattern
-    | PCoFix _ -> anomaly ~label:"head_pattern_bound" (Pp.str "not a type")
+    | PCoFix _ -> anomaly ~label:"head_pattern_bound" (Pp.str "not a type.")
 
 let head_of_constr_reference sigma c = match EConstr.kind sigma c with
   | Const (sp,_) -> ConstRef sp
   | Construct (sp,_) -> ConstructRef sp
   | Ind (sp,_) -> IndRef sp
   | Var id -> VarRef id
-  | _ -> anomaly (Pp.str "Not a rigid reference")
+  | _ -> anomaly (Pp.str "Not a rigid reference.")
 
 let pattern_of_constr env sigma t =
   let rec pattern_of_constr env t =
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 1839c87b1c..08a6dd4dbd 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -199,7 +199,7 @@ let interp_universe_level_name ~anon_rigidity evd (loc, s) =
      let names, _ = Global.global_universe_names () in
      if CString.string_contains ~where:s ~what:"." then
        match List.rev (CString.split '.' s) with
-       | [] -> anomaly (str"Invalid universe name " ++ str s)
+       | [] -> anomaly (str"Invalid universe name " ++ str s ++ str".")
        | n :: dp ->
 	  let num = int_of_string n in
 	  let dp = DirPath.make (List.map Id.of_string dp) in
@@ -1149,7 +1149,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function
                | Sort s -> ESorts.kind sigma s
                | Evar ev when is_Type (existential_type sigma ev) ->
 		   evd_comb1 (define_evar_as_sort env.ExtraEnv.env) evdref ev
-               | _ -> anomaly (Pp.str "Found a type constraint which is not a type")
+               | _ -> anomaly (Pp.str "Found a type constraint which is not a type.")
            in
 	     { utj_val = v;
 	       utj_type = s }
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 5a2328aaa4..c976fe66dd 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1445,7 +1445,7 @@ let instance sigma s c =
 let hnf_prod_app env sigma t n =
   match EConstr.kind sigma (whd_all env sigma t) with
     | Prod (_,_,b) -> subst1 n b
-    | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product")
+    | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product.")
 
 let hnf_prod_appvect env sigma t nl =
   Array.fold_left (fun acc t -> hnf_prod_app env sigma acc t) t nl
@@ -1456,7 +1456,7 @@ let hnf_prod_applist env sigma t nl =
 let hnf_lam_app env sigma t n =
   match EConstr.kind sigma (whd_all env sigma t) with
     | Lambda (_,_,b) -> subst1 n b
-    | _ -> anomaly ~label:"hnf_lam_app" (Pp.str "Need an abstraction")
+    | _ -> anomaly ~label:"hnf_lam_app" (Pp.str "Need an abstraction.")
 
 let hnf_lam_appvect env sigma t nl =
   Array.fold_left (fun acc t -> hnf_lam_app env sigma acc t) t nl
@@ -1693,5 +1693,5 @@ let betazetaevar_applist sigma n c l =
     | Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl
     | LetIn(_,b,_,c), _ -> stacklam (n-1) (substl env b::env) c stack
     | Evar _, _ -> applist (substl env t, stack)
-    | _ -> anomaly (Pp.str "Not enough lambda/let's") in
+    | _ -> anomaly (Pp.str "Not enough lambda/let's.") in
   stacklam n [] c l
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 496c706ec6..a1d0977f5a 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -48,7 +48,7 @@ let retype_error re = raise (RetypeError re)
 
 let anomaly_on_error f x =
  try f x
- with RetypeError e -> anomaly ~label:"retyping" (print_retype_error e)
+ with RetypeError e -> anomaly ~label:"retyping" (print_retype_error e ++ str ".")
 
 let get_type_from_constraints env sigma t =
   if isEvar sigma (fst (decompose_app_vect sigma t)) then
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 3d41d2ddd5..f2b0995b0b 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -107,7 +107,7 @@ let destEvalRefU sigma c = match EConstr.kind sigma c with
   | Var id  -> (EvalVar id, EInstance.empty)
   | Rel n -> (EvalRel n, EInstance.empty)
   | Evar ev -> (EvalEvar ev, EInstance.empty)
-  | _ -> anomaly (Pp.str "Not an unfoldable reference")
+  | _ -> anomaly (Pp.str "Not an unfoldable reference.")
 
 let unsafe_reference_opt_value env sigma eval =
   match eval with
@@ -307,7 +307,7 @@ let compute_consteval_mutual_fix env sigma ref =
 	  (* Forget all \'s and args and do as if we had started with c' *)
 	  let ref,_ = destEvalRefU sigma c' in
 	  (match unsafe_reference_opt_value env sigma ref with
-	    | None -> anomaly (Pp.str "Should have been trapped by compute_direct")
+	    | None -> anomaly (Pp.str "Should have been trapped by compute_direct.")
 	    | Some c -> srec env (minarg-nargs) [] ref c)
       | _ -> (* Should not occur *) NotAnElimination
   in
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 757e12451e..7ad988ad0b 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -31,7 +31,7 @@ let push_rec_types pfix env =
 let meta_type evd mv =
   let ty =
     try Evd.meta_ftype evd mv
-    with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv)) in
+    with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv) ++ str ".") in
   let ty = Evd.map_fl EConstr.of_constr ty in
   meta_instance evd ty
 
@@ -121,11 +121,11 @@ let lambda_applist_assum sigma n c l =
   let rec app n subst t l =
     if Int.equal n 0 then
       if l == [] then substl subst t
-      else anomaly (Pp.str "Not enough arguments")
+      else anomaly (Pp.str "Not enough arguments.")
     else match EConstr.kind sigma t, l with
     | Lambda(_,_,c), arg::l -> app (n-1) (arg::subst) c l
     | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l
-    | _ -> anomaly (Pp.str "Not enough lambda/let's") in
+    | _ -> anomaly (Pp.str "Not enough lambda/let's.") in
   app n [] c l
 
 let e_type_case_branches env evdref (ind,largs) pj c =