From 2ee505630756676ded9f8eb6511ad642c80179ee Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 1 Jun 2020 17:39:47 +0200
Subject: Uniformizing the "already exists" messages

---
 vernac/declaremods.ml | 2 +-
 vernac/metasyntax.ml  | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'vernac')

diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml
index 15e6d4ef37..95e05556b9 100644
--- a/vernac/declaremods.ml
+++ b/vernac/declaremods.ml
@@ -216,7 +216,7 @@ let consistency_checks exists dir dirinfo =
   else
     if Nametab.exists_dir dir then
       user_err ~hdr:"consistency_checks"
-        (DirPath.print dir ++ str " already exists")
+        (DirPath.print dir ++ str " already exists.")
 
 let compute_visibility exists i =
   if exists then Nametab.Exactly i else Nametab.Until i
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 2fe402ff08..bce208df6e 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1845,6 +1845,6 @@ let inCustomEntry : locality_flag * string -> obj =
 
 let declare_custom_entry local s =
   if Egramcoq.exists_custom_entry s then
-    user_err Pp.(str "Custom entry " ++ str s ++ str " already exists")
+    user_err Pp.(str "Custom entry " ++ str s ++ str " already exists.")
   else
     Lib.add_anonymous_leaf (inCustomEntry (local,s))
-- 
cgit v1.2.3


From 9374aeeda2a3bc64774753862eae39a8e8539bb7 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 4 Nov 2020 07:30:40 +0100
Subject: One catch-all's missing a noncritical; another is now useless (see
 7efaf86).

---
 vernac/vernacentries.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index e8d84a67a3..af40292f18 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1934,10 +1934,9 @@ let vernac_search ~pstate ~atts s gopt r =
   let open ComSearch in
   let gopt = query_command_selector gopt in
   let sigma, env =
-    match gopt with | None ->
-      (* 1st goal by default if it exists, otherwise no goal at all *)
-      (try get_goal_or_global_context ~pstate 1
-       with _ -> let env = Global.env () in (Evd.from_env env, env))
+    match gopt with
+    (* 1st goal by default if it exists, otherwise no goal at all *)
+    | None -> get_goal_or_global_context ~pstate 1
     (* if goal selector is given and wrong, then let exceptions be raised. *)
     | Some g -> get_goal_or_global_context ~pstate g in
   interp_search env sigma s r
-- 
cgit v1.2.3


From bf6a5e1c7b10d6ff5686cc4a3e71eb105d7a0473 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 31 Oct 2020 22:15:33 +0100
Subject: Missing dot in an error message.

---
 vernac/metasyntax.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac')

diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index bce208df6e..f9f65a8c30 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1664,7 +1664,7 @@ let add_notation_interpretation env decl_ntn =
       decl_ntn_scope = sc;
     } = decl_ntn in
   match interp_non_syntax_modifiers modifiers with
-  | None -> CErrors.user_err (str"Only modifiers not affecting parsing are supported here")
+  | None -> CErrors.user_err (str"Only modifiers not affecting parsing are supported here.")
   | Some (only_parsing,only_printing,entry) ->
     let df' = add_notation_interpretation_core ~local:false df env entry c sc only_parsing false None in
     Dumpglob.dump_notation (loc,df') sc true
-- 
cgit v1.2.3