1 files changed, 82 insertions, 0 deletions
diff --git a/theories/Numbers/Cyclic/Int63/PrimInt63.v b/theories/Numbers/Cyclic/Int63/PrimInt63.v
new file mode 100644
index 0000000000..64c1b862c7
--- /dev/null
+++ b/theories/Numbers/Cyclic/Int63/PrimInt63.v
@@ -0,0 +1,82 @@
+(************************************************************************)
+(*         *   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)         *)
+(************************************************************************)
+
+Require Export CarryType.
+
+Register bool as kernel.ind_bool.
+Register prod as kernel.ind_pair.
+Register carry as kernel.ind_carry.
+Register comparison as kernel.ind_cmp.
+
+Primitive int := #int63_type.
+Register int as num.int63.type.
+Declare Scope int63_scope.
+Definition id_int : int -> int := fun x => x.
+Declare ML Module "int63_syntax_plugin".
+
+Module Export Int63NotationsInternalA.
+Delimit Scope int63_scope with int63.
+Bind Scope int63_scope with int.
+End Int63NotationsInternalA.
+
+(* Logical operations *)
+Primitive lsl := #int63_lsl.
+
+Primitive lsr := #int63_lsr.
+
+Primitive land := #int63_land.
+
+Primitive lor := #int63_lor.
+
+Primitive lxor := #int63_lxor.
+
+(* Arithmetic modulo operations *)
+Primitive add := #int63_add.
+
+Primitive sub := #int63_sub.
+
+Primitive mul := #int63_mul.
+
+Primitive mulc := #int63_mulc.
+
+Primitive div := #int63_div.
+
+Primitive mod := #int63_mod.
+
+(* Comparisons *)
+Primitive eqb := #int63_eq.
+
+Primitive ltb := #int63_lt.
+
+Primitive leb := #int63_le.
+
+(** Exact arithmetic operations *)
+
+Primitive addc := #int63_addc.
+
+Primitive addcarryc := #int63_addcarryc.
+
+Primitive subc := #int63_subc.
+
+Primitive subcarryc := #int63_subcarryc.
+
+Primitive diveucl := #int63_diveucl.
+
+Primitive diveucl_21 := #int63_div21.
+
+Primitive addmuldiv := #int63_addmuldiv.
+
+(** Comparison *)
+Primitive compare := #int63_compare.
+
+(** Exotic operations *)
+
+Primitive head0 := #int63_head0.
+Primitive tail0 := #int63_tail0.