From de038270f72214b169d056642eb7144a79e6f126 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 7 Jul 2016 04:56:24 +0200
Subject: Unify location handling of error functions.

In some cases prior to this patch, there were two cases for the same
error function, one taking a location, the other not.

We unify them by using an option parameter, in the line with recent
changes in warnings and feedback.

This implies a bit of clean up in some places, but more importantly, is
the preparation for subsequent patches making `Loc.location` opaque,
change that could be use to improve modularity and allow a more
functional implementation strategy --- for example --- of the
beautifier.
---
 plugins/decl_mode/decl_interp.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/decl_mode/decl_interp.ml')

diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index a862423e99..49843d828b 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -90,7 +90,7 @@ let rec add_vars_of_simple_pattern globs = function
 (*      Loc.raise loc
 	(UserError ("simple_pattern",str "\"as\" is not allowed here"))*)
   | CPatOr (loc, _)->
-      Loc.raise loc
+      Loc.raise ~loc
 	(UserError ("simple_pattern",str "\"(_ | _)\" is not allowed here"))
   | CPatDelimiters (_,_,p) ->
       add_vars_of_simple_pattern globs p
-- 
cgit v1.2.3


From 543ee0c7ad43874c577416af9f2e5a94d7d1e4d3 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 19 Aug 2016 01:58:04 +0200
Subject: Remove errorlabstrm in favor of user_err

As noted by @ppedrot, the first is redundant. The patch is basically a renaming.

We didn't make the component optional yet, but this could happen in a
future patch.
---
 plugins/decl_mode/decl_interp.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/decl_mode/decl_interp.ml')

diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 49843d828b..9ed5c61e26 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -328,7 +328,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
   let _ =
     let expected = mib.Declarations.mind_nparams - num_params in
       if not (Int.equal (List.length params) expected) then
-	errorlabstrm "suppose it is" 
+	user_err "suppose it is" 
 	  (str "Wrong number of extra arguments: " ++ 
 	     (if Int.equal expected 0 then str "none" else int expected) ++ spc () ++
 	     str "expected.") in
@@ -348,7 +348,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
       Thesis (Plain) -> Glob_term.GSort(Loc.ghost,GProp)
     | Thesis (For rec_occ) ->
 	if not (Id.List.mem rec_occ pat_vars) then
-	  errorlabstrm "suppose it is"
+	  user_err "suppose it is"
 	    (str "Variable " ++ Nameops.pr_id rec_occ ++
 	       str " does not occur in pattern.");
 	Glob_term.GSort(Loc.ghost,GProp)
-- 
cgit v1.2.3


From fc579fdc83b751a44a18d2373e86ab38806e7306 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 19 Aug 2016 02:35:47 +0200
Subject: Make the user_err header an optional parameter.

Suggested by @ppedrot
---
 plugins/decl_mode/decl_interp.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins/decl_mode/decl_interp.ml')

diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 9ed5c61e26..f68c01b18b 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -91,7 +91,7 @@ let rec add_vars_of_simple_pattern globs = function
 	(UserError ("simple_pattern",str "\"as\" is not allowed here"))*)
   | CPatOr (loc, _)->
       Loc.raise ~loc
-	(UserError ("simple_pattern",str "\"(_ | _)\" is not allowed here"))
+	(UserError (Some "simple_pattern",str "\"(_ | _)\" is not allowed here"))
   | CPatDelimiters (_,_,p) ->
       add_vars_of_simple_pattern globs p
   | CPatCstr (_,_,pl1,pl2) ->
@@ -328,7 +328,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
   let _ =
     let expected = mib.Declarations.mind_nparams - num_params in
       if not (Int.equal (List.length params) expected) then
-	user_err "suppose it is" 
+	user_err ~hdr:"suppose it is" 
 	  (str "Wrong number of extra arguments: " ++ 
 	     (if Int.equal expected 0 then str "none" else int expected) ++ spc () ++
 	     str "expected.") in
@@ -348,7 +348,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
       Thesis (Plain) -> Glob_term.GSort(Loc.ghost,GProp)
     | Thesis (For rec_occ) ->
 	if not (Id.List.mem rec_occ pat_vars) then
-	  user_err "suppose it is"
+	  user_err ~hdr:"suppose it is"
 	    (str "Variable " ++ Nameops.pr_id rec_occ ++
 	       str " does not occur in pattern.");
 	Glob_term.GSort(Loc.ghost,GProp)
-- 
cgit v1.2.3