Imported Upstream version 8.6

1 files changed, 7 insertions, 3 deletions

diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
index fe9f1319..f65f9b79 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_syntax.ml
@@ -6,6 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(* Poor's man DECLARE PLUGIN *)
+let __coq_plugin_name = "numbers_syntax_plugin"
+let () = Mltop.add_known_module __coq_plugin_name
+
 (* digit-based syntax for int31, bigN bigZ and bigQ *)
 
 open Bigint
@@ -96,7 +100,7 @@ let int31_of_pos_bigint dloc n =
   GApp (dloc, ref_construct, List.rev (args 31 n))
 
 let error_negative dloc =
-  Errors.user_err_loc (dloc, "interp_int31", Pp.str "int31 are only non-negative numbers.")
+  CErrors.user_err_loc (dloc, "interp_int31", Pp.str "int31 are only non-negative numbers.")
 
 let interp_int31 dloc n =
   if is_pos_or_zero n then
@@ -180,12 +184,12 @@ let bigN_of_pos_bigint dloc n =
   let word = word_of_pos_bigint dloc h n in
   let args =
     if h < n_inlined then [word]
-    else [Nat_syntax.nat_of_int dloc (of_int (h-n_inlined));word]
+    else [Nat_syntax_plugin.Nat_syntax.nat_of_int dloc (of_int (h-n_inlined));word]
   in
   GApp (dloc, ref_constructor, args)
 
 let bigN_error_negative dloc =
-  Errors.user_err_loc (dloc, "interp_bigN", Pp.str "bigN are only non-negative numbers.")
+  CErrors.user_err_loc (dloc, "interp_bigN", Pp.str "bigN are only non-negative numbers.")
 
 let interp_bigN dloc n =
   if is_pos_or_zero n then