Merge PR #244.

7 files changed, 21 insertions, 21 deletions

diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index bec891f7f..f19759470 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -109,7 +109,7 @@ let get_current_file () =
 let set_current_file ~fname =
   current_file := fname
 
-let err loc str = Loc.raise (Compat.to_coqloc loc) (Error.E str)
+let err loc str = Loc.raise ~loc:(Compat.to_coqloc loc) (Error.E str)
 
 let bad_token str = raise (Error.E (Bad_token str))
 
diff --git a/parsing/compat.ml4 b/parsing/compat.ml4
index 18bc8d664..170dd7c55 100644
--- a/parsing/compat.ml4
+++ b/parsing/compat.ml4
@@ -188,7 +188,7 @@ module GrammarMake (L:LexerSig) : GrammarSig = struct
     with Exc_located (loc,e) ->
       let loc' = Loc.get_loc (Exninfo.info e) in
       let loc = match loc' with None -> to_coqloc loc | Some loc -> loc in
-      Loc.raise loc e
+      Loc.raise ~loc e
 
   let entry_print ft x = Entry.print ft x
   let srules' = Gramext.srules
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 65d49cb45..0dbe08231 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -71,7 +71,7 @@ let error_level_assoc p current expected =
     | Extend.LeftA -> str "left"
     | Extend.RightA -> str "right"
     | Extend.NonA -> str "non" in
-  errorlabstrm ""
+  user_err 
     (str "Level " ++ int p ++ str " is already declared " ++
      pr_assoc current ++ str " associative while it is now expected to be " ++
      pr_assoc expected ++ str " associative.")
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 74994c5e3..7021e5270 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -55,9 +55,9 @@ let mk_fixb (id,bl,ann,body,(loc,tyc)) =
 
 let mk_cofixb (id,bl,ann,body,(loc,tyc)) =
   let _ = Option.map (fun (aloc,_) ->
-    CErrors.user_err_loc
-      (aloc,"Constr:mk_cofixb",
-       Pp.str"Annotation forbidden in cofix expression.")) (fst ann) in
+    CErrors.user_err ~loc:aloc
+      ~hdr:"Constr:mk_cofixb"
+      (Pp.str"Annotation forbidden in cofix expression.")) (fst ann) in
   let ty = match tyc with
       Some ty -> ty
     | None -> CHole (loc, None, IntroAnonymous, None) in
@@ -380,14 +380,14 @@ GEXTEND Gram
       [ p = pattern; lp = LIST1 NEXT ->
         (match p with
 	  | CPatAtom (_, Some r) -> CPatCstr (!@loc, r, None, lp)
-	  | CPatCstr (_, r, None, l2) -> CErrors.user_err_loc
-              (cases_pattern_expr_loc p, "compound_pattern",
-               Pp.str "Nested applications not supported.")
+	  | CPatCstr (_, r, None, l2) -> CErrors.user_err
+              ~loc:(cases_pattern_expr_loc p) ~hdr:"compound_pattern"
+              (Pp.str "Nested applications not supported.")
 	  | CPatCstr (_, r, l1, l2) -> CPatCstr (!@loc, r, l1 , l2@lp)
 	  | CPatNotation (_, n, s, l) -> CPatNotation (!@loc, n , s, l@lp)
-          | _ -> CErrors.user_err_loc
-              (cases_pattern_expr_loc p, "compound_pattern",
-               Pp.str "Such pattern cannot have arguments."))
+          | _ -> CErrors.user_err
+              ~loc:(cases_pattern_expr_loc p) ~hdr:"compound_pattern"
+              (Pp.str "Such pattern cannot have arguments."))
       |"@"; r = Prim.reference; lp = LIST0 NEXT ->
         CPatCstr (!@loc, r, Some lp, []) ]
     | "1" LEFTA
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index b90e06cd3..820514b08 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -28,7 +28,7 @@ let my_int_of_string loc s =
     if n > 1024 * 2048 then raise Exit;
     n
   with Failure _ | Exit ->
-    CErrors.user_err_loc (loc,"",Pp.str "Cannot support a so large number.")
+    CErrors.user_err ~loc  (Pp.str "Cannot support a so large number.")
 
 GEXTEND Gram
   GLOBAL:
@@ -93,7 +93,7 @@ GEXTEND Gram
   ;
   ne_string:
     [ [ s = STRING ->
-        if s="" then CErrors.user_err_loc(!@loc, "", Pp.str"Empty string."); s
+        if s="" then CErrors.user_err ~loc:(!@loc) (Pp.str"Empty string."); s
     ] ]
   ;
   ne_lstring:
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 199ef9fce..3c2c45c72 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -135,9 +135,9 @@ let mk_fix_tac (loc,id,bl,ann,ty) =
 
 let mk_cofix_tac (loc,id,bl,ann,ty) =
   let _ = Option.map (fun (aloc,_) ->
-    user_err_loc
-      (aloc,"Constr:mk_cofix_tac",
-       Pp.str"Annotation forbidden in cofix expression.")) ann in
+    user_err ~loc:aloc
+      ~hdr:"Constr:mk_cofix_tac"
+      (Pp.str"Annotation forbidden in cofix expression.")) ann in
   (id,CProdN(loc,bl,ty))
 
 (* Functions overloaded by quotifier *)
@@ -192,7 +192,7 @@ let merge_occurrences loc cl = function
   | None ->
       if Locusops.clause_with_generic_occurrences cl then (None, cl)
       else
-	user_err_loc (loc,"",str "Found an \"at\" clause without \"with\" clause.")
+	user_err ~loc  (str "Found an \"at\" clause without \"with\" clause.")
   | Some (occs, p) ->
     let ans = match occs with
     | AllOccurrences -> cl
@@ -204,9 +204,9 @@ let merge_occurrences loc cl = function
         { cl with onhyps = Some [(occs, id), l] }
       | _ ->
         if Locusops.clause_with_generic_occurrences cl then
-          user_err_loc (loc,"",str "Unable to interpret the \"at\" clause; move it in the \"in\" clause.")
+          user_err ~loc  (str "Unable to interpret the \"at\" clause; move it in the \"in\" clause.")
         else
-          user_err_loc (loc,"",str "Cannot use clause \"at\" twice.")
+          user_err ~loc  (str "Cannot use clause \"at\" twice.")
       end
     in
     (Some p, ans)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index c09693b36..7cb897cf7 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -115,7 +115,7 @@ GEXTEND Gram
                     | Some (SelectNth g) -> c (Some g)
                     | None -> c None
                     | _ ->
-                        VernacError (UserError ("",str"Typing and evaluation commands, cannot be used with the \"all:\" selector."))
+                        VernacError (UserError (None,str"Typing and evaluation commands, cannot be used with the \"all:\" selector."))
                   end ] ]
   ;
   located_vernac: