Imported Upstream version 8.6upstream/8.6

18 files changed, 45 insertions, 25 deletions

diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index 67c9dd0a..e18d19ce 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -6,8 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
+(* Poor's man DECLARE PLUGIN *)
+let __coq_plugin_name = "ascii_syntax_plugin"
+let () = Mltop.add_known_module __coq_plugin_name
+
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Glob_term
diff --git a/plugins/syntax/ascii_syntax_plugin.mllib b/plugins/syntax/ascii_syntax_plugin.mllib
deleted file mode 100644
index b00f9250..00000000
--- a/plugins/syntax/ascii_syntax_plugin.mllib
+++ /dev/null
@@ -1,2 +0,0 @@
-Ascii_syntax
-Ascii_syntax_plugin_mod
diff --git a/plugins/syntax/ascii_syntax_plugin.mlpack b/plugins/syntax/ascii_syntax_plugin.mlpack
new file mode 100644
index 00000000..7b9213a0
--- /dev/null
+++ b/plugins/syntax/ascii_syntax_plugin.mlpack
@@ -0,0 +1 @@
+Ascii_syntax
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
index 5f44904c..a9eb126b 100644
--- a/plugins/syntax/nat_syntax.ml
+++ b/plugins/syntax/nat_syntax.ml
@@ -6,6 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(* Poor's man DECLARE PLUGIN *)
+let __coq_plugin_name = "nat_syntax_plugin"
+let () = Mltop.add_known_module __coq_plugin_name
+
 (* This file defines the printer for natural numbers in [nat] *)
 
 (*i*)
@@ -13,7 +17,7 @@ open Glob_term
 open Bigint
 open Coqlib
 open Pp
-open Errors
+open CErrors
 (*i*)
 
 (**********************************************************************)
@@ -22,14 +26,16 @@ open Errors
 
 let threshold = of_int 5000
 
+let warn_large_nat =
+  CWarnings.create ~name:"large-nat" ~category:"numbers"
+    (fun () -> strbrk "Stack overflow or segmentation fault happens when " ++
+                 strbrk "working with large numbers in nat (observed threshold " ++
+                 strbrk "may vary from 5000 to 70000 depending on your system " ++
+                 strbrk "limits and on the command executed).")
+
 let nat_of_int dloc n =
   if is_pos_or_zero n then begin
-      if less_than threshold n then
-	msg_warning
-	  (strbrk "Stack overflow or segmentation fault happens when " ++
-	   strbrk "working with large numbers in nat (observed threshold " ++
-	   strbrk "may vary from 5000 to 70000 depending on your system " ++
-	   strbrk "limits and on the command executed).");
+      if less_than threshold n then warn_large_nat ();
       let ref_O = GRef (dloc, glob_O, None) in
       let ref_S = GRef (dloc, glob_S, None) in
       let rec mk_nat acc n =
diff --git a/plugins/syntax/nat_syntax_plugin.mllib b/plugins/syntax/nat_syntax_plugin.mllib
deleted file mode 100644
index 69b0cb20..00000000
--- a/plugins/syntax/nat_syntax_plugin.mllib
+++ /dev/null
@@ -1,2 +0,0 @@
-Nat_syntax
-Nat_syntax_plugin_mod
diff --git a/plugins/syntax/nat_syntax_plugin.mlpack b/plugins/syntax/nat_syntax_plugin.mlpack
new file mode 100644
index 00000000..39bdd62f
--- /dev/null
+++ b/plugins/syntax/nat_syntax_plugin.mlpack
@@ -0,0 +1 @@
+Nat_syntax
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
diff --git a/plugins/syntax/numbers_syntax_plugin.mllib b/plugins/syntax/numbers_syntax_plugin.mllib
deleted file mode 100644
index ebc0bb20..00000000
--- a/plugins/syntax/numbers_syntax_plugin.mllib
+++ /dev/null
@@ -1,2 +0,0 @@
-Numbers_syntax
-Numbers_syntax_plugin_mod
diff --git a/plugins/syntax/numbers_syntax_plugin.mlpack b/plugins/syntax/numbers_syntax_plugin.mlpack
new file mode 100644
index 00000000..e48c00a0
--- /dev/null
+++ b/plugins/syntax/numbers_syntax_plugin.mlpack
@@ -0,0 +1 @@
+Numbers_syntax
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index 05d73f9e..3ae2d45f 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -10,6 +10,10 @@ open Util
 open Names
 open Globnames
 
+(* Poor's man DECLARE PLUGIN *)
+let __coq_plugin_name = "r_syntax_plugin"
+let () = Mltop.add_known_module __coq_plugin_name
+
 exception Non_closed_number
 
 (**********************************************************************)
diff --git a/plugins/syntax/r_syntax_plugin.mllib b/plugins/syntax/r_syntax_plugin.mllib
deleted file mode 100644
index 5c173a14..00000000
--- a/plugins/syntax/r_syntax_plugin.mllib
+++ /dev/null
@@ -1,2 +0,0 @@
-R_syntax
-R_syntax_plugin_mod
diff --git a/plugins/syntax/r_syntax_plugin.mlpack b/plugins/syntax/r_syntax_plugin.mlpack
new file mode 100644
index 00000000..d4ee75ea
--- /dev/null
+++ b/plugins/syntax/r_syntax_plugin.mlpack
@@ -0,0 +1 @@
+R_syntax
diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
index 2e696f39..de0fa77e 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -7,10 +7,14 @@
 (***********************************************************************)
 
 open Globnames
-open Ascii_syntax
+open Ascii_syntax_plugin.Ascii_syntax
 open Glob_term
 open Coqlib
 
+(* Poor's man DECLARE PLUGIN *)
+let __coq_plugin_name = "string_syntax_plugin"
+let () = Mltop.add_known_module __coq_plugin_name
+
 exception Non_closed_string
 
 (* make a string term from the string s *)
diff --git a/plugins/syntax/string_syntax_plugin.mllib b/plugins/syntax/string_syntax_plugin.mllib
deleted file mode 100644
index b108c9e0..00000000
--- a/plugins/syntax/string_syntax_plugin.mllib
+++ /dev/null
@@ -1,2 +0,0 @@
-String_syntax
-String_syntax_plugin_mod
diff --git a/plugins/syntax/string_syntax_plugin.mlpack b/plugins/syntax/string_syntax_plugin.mlpack
new file mode 100644
index 00000000..45d6e0fa
--- /dev/null
+++ b/plugins/syntax/string_syntax_plugin.mlpack
@@ -0,0 +1 @@
+String_syntax
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index 53c1b5d7..60803a36 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -7,11 +7,15 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Bigint
 
+(* Poor's man DECLARE PLUGIN *)
+let __coq_plugin_name = "z_syntax_plugin"
+let () = Mltop.add_known_module __coq_plugin_name
+
 exception Non_closed_number
 
 (**********************************************************************)
diff --git a/plugins/syntax/z_syntax_plugin.mllib b/plugins/syntax/z_syntax_plugin.mllib
deleted file mode 100644
index 36d41acc..00000000
--- a/plugins/syntax/z_syntax_plugin.mllib
+++ /dev/null
@@ -1,2 +0,0 @@
-Z_syntax
-Z_syntax_plugin_mod
diff --git a/plugins/syntax/z_syntax_plugin.mlpack b/plugins/syntax/z_syntax_plugin.mlpack
new file mode 100644
index 00000000..411260c0
--- /dev/null
+++ b/plugins/syntax/z_syntax_plugin.mlpack
@@ -0,0 +1 @@
+Z_syntax