Signed primitive integers

Signed primitive integers defined on top of the existing unsigned ones
with two's complement.

The module Sint63 includes the theory of signed primitive integers that
differs from the unsigned case.

Additions to the kernel:
  les (signed <=), lts (signed <), compares (signed compare),
  divs (signed division), rems (signed remainder),
  asr (arithmetic shift right)
(The s suffix is not used when importing the Sint63 module.)

The printing and parsing of primitive ints was updated and the
int63_syntax_plugin was removed (we use Number Notation instead).

A primitive int is parsed / printed as unsigned or signed depending on
the scope. In the default (Set Printing All) case, it is printed in
hexadecimal.

1 files changed, 0 insertions, 58 deletions

diff --git a/plugins/syntax/int63_syntax.ml b/plugins/syntax/int63_syntax.ml
deleted file mode 100644
index 110b26581f..0000000000
--- a/plugins/syntax/int63_syntax.ml
+++ /dev/null
@@ -1,58 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-
-(* Poor's man DECLARE PLUGIN *)
-let __coq_plugin_name = "int63_syntax_plugin"
-let () = Mltop.add_known_module __coq_plugin_name
-
-(* digit-based syntax for int63 *)
-
-open Names
-open Libnames
-
-(*** Constants for locating int63 constructors ***)
-
-let q_int63 = qualid_of_string "Coq.Numbers.Cyclic.Int63.PrimInt63.int"
-let q_id_int63 = qualid_of_string "Coq.Numbers.Cyclic.Int63.PrimInt63.id_int"
-
-let make_dir l = DirPath.make (List.rev_map Id.of_string l)
-let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
-
-(* int63 stuff *)
-let int63_module = ["Coq"; "Numbers"; "Cyclic"; "Int63"; "PrimInt63"]
-let int63_path = make_path int63_module "int"
-let int63_scope = "int63_scope"
-
-let at_declare_ml_module f x =
-  Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name
-
-(* Actually declares the interpreter for int63 *)
-
-let _ =
-  let open Notation in
-  at_declare_ml_module
-    (fun () ->
-       let id_int63 = Nametab.locate q_id_int63 in
-       let o = { to_kind = Int63, Direct;
-                 to_ty = id_int63;
-                 to_post = [||];
-                 of_kind = Int63, Direct;
-                 of_ty = id_int63;
-                 ty_name = q_int63;
-                 warning = Nop } in
-       enable_prim_token_interpretation
-         { pt_local = false;
-           pt_scope = int63_scope;
-           pt_interp_info = NumberNotation o;
-           pt_required = (int63_path, int63_module);
-           pt_refs = [];
-           pt_in_match = false })
-    ()