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

4 files changed, 17 insertions, 17 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 19be62972..19ca8d50b 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -700,7 +700,7 @@ let rec extern inctx scopes vars r =
 		     | None :: q -> raise No_match
 		     | Some c :: q ->
 		         match locs with
-			   | [] -> anomaly (Pp.str "projections corruption [Constrextern.extern]")
+			   | [] -> anomaly (Pp.str "projections corruption [Constrextern.extern].")
 			   | (_, false) :: locs' ->
 			       (* we don't want to print locals *)
 			       ip q locs' args acc
@@ -1035,7 +1035,7 @@ let rec glob_of_pat env sigma pat = CAst.make @@ match pat with
       let id = try match lookup_name_of_rel n env with
 	| Name id   -> id
 	| Anonymous ->
-	    anomaly ~label:"glob_constr_of_pattern" (Pp.str "index to an anonymous variable")
+	    anomaly ~label:"glob_constr_of_pattern" (Pp.str "index to an anonymous variable.")
       with Not_found -> Id.of_string ("_UNBOUND_REL_"^(string_of_int n)) in
       GVar id
   | PMeta None -> GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous,None)
@@ -1066,7 +1066,7 @@ let rec glob_of_pat env sigma pat = CAst.make @@ match pat with
 	| _, Some ind ->
 	  let bl' = List.map (fun (i,n,c) -> (i,n,glob_of_pat env sigma c)) bl in
 	  simple_cases_matrix_of_branches ind bl'
-	| _, None -> anomaly (Pp.str "PCase with some branches but unknown inductive")
+	| _, None -> anomaly (Pp.str "PCase with some branches but unknown inductive.")
       in
       let mat = if info.cip_extensible then mat @ [any_any_branch] else mat
       in
@@ -1074,7 +1074,7 @@ let rec glob_of_pat env sigma pat = CAst.make @@ match pat with
 	| PMeta None, _, _ -> (Anonymous,None),None
 	| _, Some ind, Some nargs ->
 	  return_type_of_predicate ind nargs (glob_of_pat env sigma p)
-	| _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive")
+	| _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive.")
       in
       GCases (RegularStyle,rtn,[glob_of_pat env sigma tm,indnames],mat)
   | PFix f -> (Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkFix f))).v (** FIXME bad env *)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 120258b45..336cfac85 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -616,7 +616,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
 	  let env,bl' = List.fold_left (intern_local_binder_aux intern ntnvars) (env,[]) bl in
           terms_of_binders (if lassoc then bl' else List.rev bl'),(None,[])
         with Not_found ->
-          anomaly (Pp.str "Inconsistent substitution of recursive notation") in
+          anomaly (Pp.str "Inconsistent substitution of recursive notation.") in
       let termin = aux (terms,None,None) subinfos terminator in
       let fold a t =
         let nterms = Id.Map.add y (a, (scopt, subscopes)) terms in
@@ -659,7 +659,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
 	  termin bl in
 	make_letins letins res
       with Not_found ->
-          anomaly (Pp.str "Inconsistent substitution of recursive notation"))
+          anomaly (Pp.str "Inconsistent substitution of recursive notation."))
     | NProd (Name id, NHole _, c') when option_mem_assoc id binderopt ->
         let a,letins = snd (Option.get binderopt) in
         let e = make_letins letins (aux subst' infos c') in
@@ -1070,7 +1070,7 @@ let sort_fields ~complete loc fields completer =
           let global_record_id = ConstructRef record.Recordops.s_CONST in
           try Qualid (loc, shortest_qualid_of_global Id.Set.empty global_record_id)
           with Not_found ->
-            anomaly (str "Environment corruption for records") in
+            anomaly (str "Environment corruption for records.") in
         let () = check_duplicate loc fields in
         let (end_index,    (* one past the last field index *)
              first_field_index,  (* index of the first field of the record *)
@@ -1085,7 +1085,7 @@ let sort_fields ~complete loc fields completer =
                  let field_glob_ref = ConstRef field_glob_id in
                  let first_field = eq_gr field_glob_ref first_field_glob_ref in
                  begin match proj_kinds with
-                    | [] -> anomaly (Pp.str "Number of projections mismatch")
+                    | [] -> anomaly (Pp.str "Number of projections mismatch.")
                     | (_, regular) :: proj_kinds ->
                        (* "regular" is false when the field is defined
                            by a let-in in the record declaration
@@ -1218,7 +1218,7 @@ let drop_notations_pattern looked_for =
     | GHole (_,_,_) -> RCPatAtom (None)
     | GRef (g,_) -> RCPatCstr (g,[],[])
     | GApp ({ v = GRef (g,_) }, l) -> RCPatCstr (g, List.map rcp_of_glob l,[])
-    | _ -> CErrors.anomaly Pp.(str "Invalid return pattern from Notation.interp_prim_token_cases_pattern_expr "))) x
+    | _ -> CErrors.anomaly Pp.(str "Invalid return pattern from Notation.interp_prim_token_cases_pattern_expr."))) x
   in
   let rec drop_syndef top scopes re pats =
     let (loc,qid) = qualid_of_reference re in
@@ -1345,7 +1345,7 @@ let drop_notations_pattern looked_for =
 	  in_pat top (scopt,subscopes@snd scopes) a
 	with Not_found ->
 	  if Id.equal id ldots_var then CAst.make ?loc @@ RCPatAtom (Some id) else
-	    anomaly (str "Unbound pattern notation variable: " ++ Id.print id)
+	    anomaly (str "Unbound pattern notation variable: " ++ Id.print id ++ str ".")
       end
     | NRef g ->
       ensure_kind top loc g;
@@ -1370,7 +1370,7 @@ let drop_notations_pattern looked_for =
            subst_pat_iterator ldots_var t u)
            (if lassoc then List.rev l else l) termin
        with Not_found ->
-         anomaly (Pp.str "Inconsistent substitution of recursive notation"))
+         anomaly (Pp.str "Inconsistent substitution of recursive notation."))
     | NHole _ ->
       let () = assert (List.is_empty args) in
       CAst.make ?loc @@ RCPatAtom None
@@ -1464,7 +1464,7 @@ let get_implicit_name n imps =
 let set_hole_implicit i b = function
   | {loc; v = GRef (r,_) } | { v = GApp ({loc; v = GRef (r,_)},_) } -> Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),Misctypes.IntroAnonymous,None)
   | {loc; v = GVar id } -> Loc.tag ?loc (Evar_kinds.ImplicitArg (VarRef id,i,b),Misctypes.IntroAnonymous,None)
-  | _ -> anomaly (Pp.str "Only refs have implicits")
+  | _ -> anomaly (Pp.str "Only refs have implicits.")
 
 let exists_implicit_name id =
   List.exists (fun imp -> is_status_implicit imp && Id.equal id (name_of_implicit imp))
diff --git a/interp/notation.ml b/interp/notation.ml
index d19654b10..23332f7c4 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -381,7 +381,7 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function
 
 let declare_notation_level ntn level =
   if String.Map.mem ntn !notation_level_map then
-    anomaly (str "Notation " ++ str ntn ++ str " is already assigned a level");
+    anomaly (str "Notation " ++ str ntn ++ str " is already assigned a level.");
   notation_level_map := String.Map.add ntn level !notation_level_map
 
 let level_of_notation ntn =
@@ -1004,13 +1004,13 @@ let declare_notation_rule ntn ~extra unpl gram =
 
 let find_notation_printing_rule ntn =
   try pi1 (String.Map.find ntn !notation_rules)
-  with Not_found -> anomaly (str "No printing rule found for " ++ str ntn)
+  with Not_found -> anomaly (str "No printing rule found for " ++ str ntn ++ str ".")
 let find_notation_extra_printing_rules ntn =
   try pi2 (String.Map.find ntn !notation_rules)
   with Not_found -> []
 let find_notation_parsing_rules ntn =
   try pi3 (String.Map.find ntn !notation_rules)
-  with Not_found -> anomaly (str "No parsing rule found for " ++ str ntn)
+  with Not_found -> anomaly (str "No parsing rule found for " ++ str ntn ++ str ".")
 
 let get_defined_notations () =
   String.Set.elements @@ String.Map.domain !notation_rules
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 8e876ec16..08b9fbe8e 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -690,7 +690,7 @@ let bind_term_as_binding_env alp (terms,onlybinders,termlists,binderlists as sig
     | { CAst.v = GVar id' } ->
        (if not (Id.equal id id') then (fst alp,(id,id')::snd alp) else alp),
        sigma
-    | _ -> anomaly (str "A term which can be a binder has to be a variable")
+    | _ -> anomaly (str "A term which can be a binder has to be a variable.")
   with Not_found ->
     (* The matching against a term allowing to find the instance has not been found yet *)
     (* If it will be a different name, we shall unfortunately fail *)
@@ -830,7 +830,7 @@ let bind_bindinglist_as_term_env alp (terms,onlybinders,termlists,binderlists) v
     let sigma = (terms,onlybinders,termlists,Id.List.remove_assoc var binderlists) in
     add_bindinglist_env sigma var bl
   with Not_found ->
-    anomaly (str "There should be a binder list bindings this list of terms")
+    anomaly (str "There should be a binder list bindings this list of terms.")
 
 let match_fix_kind fk1 fk2 =
   match (fk1,fk2) with