aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitlab-ci.yml107
-rw-r--r--doc/sphinx/_static/notations.css10
-rw-r--r--doc/stdlib/index-list.html.template2
-rw-r--r--plugins/syntax/int63_syntax.ml6
-rw-r--r--test-suite/output/Int63Syntax.out22
-rw-r--r--test-suite/output/Int63Syntax.v16
-rw-r--r--test-suite/primitive/uint63/addcarryc.v2
-rw-r--r--test-suite/primitive/uint63/addmuldiv.v2
-rw-r--r--test-suite/primitive/uint63/diveucl.v2
-rw-r--r--test-suite/primitive/uint63/head0.v2
-rw-r--r--test-suite/primitive/uint63/subcarryc.v2
-rw-r--r--test-suite/primitive/uint63/tail0.v2
-rw-r--r--theories/Floats/PrimFloat.v2
-rw-r--r--theories/Numbers/Cyclic/Abstract/CarryType.v18
-rw-r--r--theories/Numbers/Cyclic/Abstract/DoubleType.v8
-rw-r--r--theories/Numbers/Cyclic/Int63/Int63.v88
-rw-r--r--theories/Numbers/Cyclic/Int63/PrimInt63.v82
17 files changed, 184 insertions, 189 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index af54edfa21..749b74d584 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -9,11 +9,11 @@ stages:
- stage-5 # Only dependencies in stage 1, 2, 3, and 4
- deploy
-# When a job has no dependencies, it goes to stage 1. Otherwise, we
-# set both "needs" and "dependencies". "needs" is a superset of
-# "dependencies" that should include all the transitive dependencies.
-# "dependencies" only list the previous jobs whose artifact we need to
-# keep.
+# When a job has no dependencies, it goes to stage 1. Otherwise, we
+# set "needs" to contain all transitive dependencies (with "artifacts:
+# false" when we don't want the artifacts). We include the transitive
+# dependencies due to gitlab bugs sometimes starting the job even if a
+# transitive dep failed, see #10699 / 7b59d8c9d9b2104de7162ec0e40f6182a6830046.
# some default values
variables:
@@ -112,7 +112,6 @@ before_script:
variables:
- $ONLY_WINDOWS == "true"
interruptible: true
- dependencies: []
script:
# flambda can be pretty stack hungry, specially with -O3
# See also https://github.com/ocaml/ocaml/issues/7842#issuecomment-596863244
@@ -141,8 +140,6 @@ before_script:
interruptible: true
needs:
- build:edge+flambda:dune:dev
- dependencies:
- - build:edge+flambda:dune:dev
script:
- tar xfj _build.tar.bz2
- set -e
@@ -158,7 +155,7 @@ before_script:
name: "$CI_JOB_NAME"
expire_in: 2 months
-# every non build job must set dependencies otherwise all build
+# every non build job must set "needs" otherwise all build
# artifacts are used together and we may get some random Coq. To that
# purpose, we add a spurious dependency `not-a-real-job` that must be
# overridden otherwise the CI will fail.
@@ -169,7 +166,7 @@ before_script:
variables:
- $ONLY_WINDOWS == "true"
interruptible: true
- dependencies:
+ needs:
- not-a-real-job
script:
- SPHINXENV='COQBIN="'"$PWD"'/_install_ci/bin/"'
@@ -181,14 +178,14 @@ before_script:
- _install_ci/share/doc/coq/
expire_in: 2 months
-# set dependencies when using
+# set "needs" when using
.test-suite-template:
stage: stage-2
except:
variables:
- $ONLY_WINDOWS == "true"
interruptible: true
- dependencies:
+ needs:
- not-a-real-job
script:
- cd test-suite
@@ -206,14 +203,14 @@ before_script:
# Gitlab doesn't support yet "expire_in: never" so we use the instance default
# expire_in: never
-# set dependencies when using
+# set "needs" when using
.validate-template:
stage: stage-2
except:
variables:
- $ONLY_WINDOWS == "true"
interruptible: true
- dependencies:
+ needs:
- not-a-real-job
script:
# exit 0: workaround for https://gitlab.com/gitlab-org/gitlab/issues/202505
@@ -249,15 +246,11 @@ before_script:
when: always
needs:
- build:base
- dependencies:
- - build:base
.ci-template-flambda:
extends: .ci-template
needs:
- build:edge+flambda
- dependencies:
- - build:edge+flambda
variables:
OPAM_SWITCH: "edge"
OPAM_VARIANT: "+flambda"
@@ -271,7 +264,6 @@ before_script:
- artifacts
when: always
expire_in: 1 week
- dependencies: []
tags:
- windows-inria
before_script: []
@@ -373,7 +365,6 @@ lint:
variables:
- $ONLY_WINDOWS == "true"
script: dev/lint-repository.sh
- dependencies: []
variables:
GIT_DEPTH: "" # we need an unknown amount of history for per-commit linting
OPAM_SWITCH: "edge"
@@ -386,7 +377,6 @@ pkg:opam:
- $ONLY_WINDOWS == "true"
interruptible: true
# OPAM will build out-of-tree so no point in importing artifacts
- dependencies: []
script:
- set -e
- opam pin add --kind=path coq.dev .
@@ -410,7 +400,6 @@ pkg:opam:
GIT_STRATEGY: none
NIXOS_PUBLIC_KEY: cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY=
- dependencies: [] # We don't need to download build artifacts
before_script: [] # We don't want to use the shared 'before_script'
script:
- cat /proc/{cpu,mem}info || true
@@ -454,7 +443,6 @@ pkg:nix:deploy:channel:
- /^v.*\..*$/
variables:
- $CACHIX_DEPLOYMENT_KEY
- dependencies: []
needs:
- pkg:nix:deploy
script:
@@ -476,8 +464,6 @@ pkg:nix:
doc:refman:
extends: .doc-template
- dependencies:
- - build:base
needs:
- build:base
@@ -518,10 +504,6 @@ doc:refman:deploy:
only:
variables:
- $DOCUMENTATION_DEPLOY_KEY
- dependencies:
- - doc:ml-api:odoc
- - doc:refman:dune
- - build:base
needs:
- doc:ml-api:odoc
- doc:refman:dune
@@ -552,15 +534,11 @@ doc:ml-api:odoc:
test-suite:base:
extends: .test-suite-template
- dependencies:
- - build:base
needs:
- build:base
test-suite:base+32bit:
extends: .test-suite-template
- dependencies:
- - build:base+32bit
needs:
- build:base+32bit
variables:
@@ -569,8 +547,6 @@ test-suite:base+32bit:
test-suite:edge+flambda:
extends: .test-suite-template
- dependencies:
- - build:edge+flambda
needs:
- build:edge+flambda
variables:
@@ -584,8 +560,6 @@ test-suite:edge:dune:dev:
variables:
- $ONLY_WINDOWS == "true"
interruptible: true
- dependencies:
- - build:edge+flambda:dune:dev
needs:
- build:edge+flambda:dune:dev
script:
@@ -608,7 +582,6 @@ test-suite:edge:dune:dev:
variables:
- $ONLY_WINDOWS == "true"
interruptible: true
- dependencies: []
script:
- opam switch create $OCAMLVER --empty
- eval $(opam env)
@@ -637,8 +610,6 @@ test-suite:edge:dune:dev:
test-suite:base+async:
extends: .test-suite-template
- dependencies:
- - build:base
needs:
- build:base
variables:
@@ -651,15 +622,11 @@ test-suite:base+async:
validate:base:
extends: .validate-template
- dependencies:
- - build:base
needs:
- build:base
validate:base+32bit:
extends: .validate-template
- dependencies:
- - build:base+32bit
needs:
- build:base+32bit
variables:
@@ -668,8 +635,6 @@ validate:base+32bit:
validate:edge+flambda:
extends: .validate-template
- dependencies:
- - build:edge+flambda
needs:
- build:edge+flambda
variables:
@@ -679,8 +644,6 @@ validate:edge+flambda:
validate:quick:
extends: .validate-template
- dependencies:
- - build:quick
needs:
- build:quick
only:
@@ -707,9 +670,6 @@ library:ci-color:
needs:
- build:edge+flambda
- plugin:ci-bignums
- dependencies:
- - build:edge+flambda
- - plugin:ci-bignums
library:ci-compcert:
stage: stage-3
@@ -731,9 +691,6 @@ library:ci-coqprime:
needs:
- build:edge+flambda
- plugin:ci-bignums
- dependencies:
- - build:edge+flambda
- - plugin:ci-bignums
library:ci-coqtail:
extends: .ci-template
@@ -744,9 +701,6 @@ library:ci-coquelicot:
needs:
- build:edge+flambda
- library:ci-mathcomp
- dependencies:
- - build:edge+flambda
- - library:ci-mathcomp
library:ci-cross_crypto:
extends: .ci-template
@@ -765,11 +719,6 @@ library:ci-fiat_crypto:
- library:ci-coqprime
- plugin:ci-bignums
- plugin:ci-rewriter
- dependencies:
- - build:edge+flambda
- - library:ci-coqprime
- - plugin:ci-bignums
- - plugin:ci-rewriter
library:ci-fiat_crypto_legacy:
extends: .ci-template-flambda
@@ -787,12 +736,6 @@ library:ci-fiat_crypto_ocaml:
- plugin:ci-bignums
- plugin:ci-rewriter
- library:ci-fiat_crypto
- dependencies:
- - build:edge+flambda
- - library:ci-coqprime
- - plugin:ci-bignums
- - plugin:ci-rewriter
- - library:ci-fiat_crypto
library:ci-flocq:
extends: .ci-template-flambda
@@ -809,12 +752,6 @@ library:ci-interval:
- library:ci-flocq
- library:ci-mathcomp
- plugin:ci-bignums
- dependencies:
- - build:edge+flambda
- - library:ci-coquelicot
- - library:ci-flocq
- - library:ci-mathcomp
- - plugin:ci-bignums
library:ci-oddorder:
extends: .ci-template-flambda
@@ -822,9 +759,6 @@ library:ci-oddorder:
needs:
- build:edge+flambda
- library:ci-mathcomp
- dependencies:
- - build:edge+flambda
- - library:ci-mathcomp
library:ci-fourcolor:
extends: .ci-template-flambda
@@ -832,9 +766,6 @@ library:ci-fourcolor:
needs:
- build:edge+flambda
- library:ci-mathcomp
- dependencies:
- - build:edge+flambda
- - library:ci-mathcomp
library:ci-corn:
extends: .ci-template-flambda
@@ -843,9 +774,6 @@ library:ci-corn:
- build:edge+flambda
- plugin:ci-bignums
- library:ci-math_classes
- dependencies:
- - build:edge+flambda
- - library:ci-math_classes
plugin:ci-gappa:
extends: .ci-template-flambda
@@ -853,9 +781,6 @@ plugin:ci-gappa:
needs:
- build:edge+flambda
- library:ci-flocq
- dependencies:
- - build:edge+flambda
- - library:ci-flocq
library:ci-geocoq:
extends: .ci-template-flambda
@@ -872,9 +797,6 @@ library:ci-math_classes:
needs:
- build:edge+flambda
- plugin:ci-bignums
- dependencies:
- - build:edge+flambda
- - plugin:ci-bignums
library:ci-mathcomp:
extends: .ci-template-flambda
@@ -900,9 +822,6 @@ library:ci-vst:
needs:
- build:edge+flambda
- library:ci-flocq
- dependencies:
- - build:edge+flambda
- - library:ci-flocq
# Plugins are by definition the projects that depend on Coq's ML API
@@ -933,9 +852,6 @@ plugin:ci-metacoq:
needs:
- build:base
- plugin:ci-equations
- dependencies:
- - build:base
- - plugin:ci-equations
plugin:ci-mtac2:
extends: .ci-template
@@ -952,7 +868,6 @@ plugin:plugin-tutorial:
variables:
- $ONLY_WINDOWS == "true"
interruptible: true
- dependencies: []
script:
- ./configure -local -warn-error yes
- make -j "$NJOBS" plugin-tutorial
diff --git a/doc/sphinx/_static/notations.css b/doc/sphinx/_static/notations.css
index 8c3f7ac3c1..abb08d98cc 100644
--- a/doc/sphinx/_static/notations.css
+++ b/doc/sphinx/_static/notations.css
@@ -266,3 +266,13 @@ code span.error {
.rst-content tt.literal, .rst-content tt.literal, .rst-content code.literal {
color: inherit !important;
}
+
+/* make the error message index readable */
+.indextable code {
+ white-space: inherit; /* break long lines */
+}
+
+.indextable tr td + td {
+ padding-left: 2em; /* indent 2nd & subsequent lines */
+ text-indent: -2em;
+}
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 8ab4265b15..cbe526be68 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -278,11 +278,13 @@ through the <tt>Require Import</tt> command.</p>
<dd>
theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
theories/Numbers/Cyclic/Abstract/NZCyclic.v
+ theories/Numbers/Cyclic/Abstract/CarryType.v
theories/Numbers/Cyclic/Abstract/DoubleType.v
theories/Numbers/Cyclic/Int31/Cyclic31.v
theories/Numbers/Cyclic/Int31/Ring31.v
theories/Numbers/Cyclic/Int31/Int31.v
theories/Numbers/Cyclic/Int63/Cyclic63.v
+ theories/Numbers/Cyclic/Int63/PrimInt63.v
theories/Numbers/Cyclic/Int63/Int63.v
theories/Numbers/Cyclic/Int63/Ring63.v
theories/Numbers/Cyclic/ZModulo/ZModulo.v
diff --git a/plugins/syntax/int63_syntax.ml b/plugins/syntax/int63_syntax.ml
index b14b02f3bb..110b26581f 100644
--- a/plugins/syntax/int63_syntax.ml
+++ b/plugins/syntax/int63_syntax.ml
@@ -20,14 +20,14 @@ open Libnames
(*** Constants for locating int63 constructors ***)
-let q_int63 = qualid_of_string "Coq.Numbers.Cyclic.Int63.Int63.int"
-let q_id_int63 = qualid_of_string "Coq.Numbers.Cyclic.Int63.Int63.id_int"
+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"; "Int63"]
+let int63_module = ["Coq"; "Numbers"; "Cyclic"; "Int63"; "PrimInt63"]
let int63_path = make_path int63_module "int"
let int63_scope = "int63_scope"
diff --git a/test-suite/output/Int63Syntax.out b/test-suite/output/Int63Syntax.out
index eefa338f0d..ca8e1b58a8 100644
--- a/test-suite/output/Int63Syntax.out
+++ b/test-suite/output/Int63Syntax.out
@@ -1,7 +1,5 @@
2%int63
: int
-(2 + 2)%int63
- : int
2
: int
9223372036854775807
@@ -17,9 +15,9 @@
427
: int
The command has indeed failed with message:
-Cannot interpret this number as a value of type Coq.Numbers.Cyclic.Int63.Int63.int
+Cannot interpret this number as a value of type Coq.Numbers.Cyclic.Int63.PrimInt63.int
The command has indeed failed with message:
-Cannot interpret this number as a value of type Coq.Numbers.Cyclic.Int63.Int63.int
+Cannot interpret this number as a value of type Coq.Numbers.Cyclic.Int63.PrimInt63.int
0
: int
0
@@ -32,13 +30,7 @@ The command has indeed failed with message:
The reference x1 was not found in the current environment.
The command has indeed failed with message:
The reference x was not found in the current environment.
-2 + 2
- : int
-2 + 2
- : int
- = 4
- : int
- = 37151199385380486
+add 2 2
: int
The command has indeed failed with message:
int63 are only non-negative numbers.
@@ -56,3 +48,11 @@ t = 2%i63
: nat
2
: int
+(2 + 2)%int63
+ : int
+2 + 2
+ : int
+ = 4
+ : int
+ = 37151199385380486
+ : int
diff --git a/test-suite/output/Int63Syntax.v b/test-suite/output/Int63Syntax.v
index c49616d918..6f1046f7a5 100644
--- a/test-suite/output/Int63Syntax.v
+++ b/test-suite/output/Int63Syntax.v
@@ -1,7 +1,6 @@
-Require Import Int63 Cyclic63.
+Require Import PrimInt63.
Check 2%int63.
-Check (2 + 2)%int63.
Open Scope int63_scope.
Check 2.
Check 9223372036854775807.
@@ -18,10 +17,7 @@ Fail Check 0xg.
Fail Check 0xG.
Fail Check 00x1.
Fail Check 0x.
-Check (Int63.add 2 2).
-Check (2+2).
-Eval vm_compute in 2+2.
-Eval vm_compute in 65675757 * 565675998.
+Check (PrimInt63.add 2 2).
Fail Check -1.
Fail Check 9223372036854775808.
Open Scope nat_scope.
@@ -36,3 +32,11 @@ Check 2.
Close Scope nat_scope.
Check 2.
Close Scope int63_scope.
+
+Require Import Int63.
+
+Check (2 + 2)%int63.
+Open Scope int63_scope.
+Check (2+2).
+Eval vm_compute in 2+2.
+Eval vm_compute in 65675757 * 565675998.
diff --git a/test-suite/primitive/uint63/addcarryc.v b/test-suite/primitive/uint63/addcarryc.v
index a4430769ca..7ab3af51d8 100644
--- a/test-suite/primitive/uint63/addcarryc.v
+++ b/test-suite/primitive/uint63/addcarryc.v
@@ -1,4 +1,4 @@
-Require Import Int63.
+Require Import PrimInt63.
Set Implicit Arguments.
diff --git a/test-suite/primitive/uint63/addmuldiv.v b/test-suite/primitive/uint63/addmuldiv.v
index 72b0164b49..e3aded6c96 100644
--- a/test-suite/primitive/uint63/addmuldiv.v
+++ b/test-suite/primitive/uint63/addmuldiv.v
@@ -1,4 +1,4 @@
-Require Import Int63.
+Require Import PrimInt63.
Set Implicit Arguments.
diff --git a/test-suite/primitive/uint63/diveucl.v b/test-suite/primitive/uint63/diveucl.v
index 8f88a0f356..43a0741ffe 100644
--- a/test-suite/primitive/uint63/diveucl.v
+++ b/test-suite/primitive/uint63/diveucl.v
@@ -1,4 +1,4 @@
-Require Import Int63.
+Require Import PrimInt63.
Set Implicit Arguments.
diff --git a/test-suite/primitive/uint63/head0.v b/test-suite/primitive/uint63/head0.v
index f4234d2605..30cbce4537 100644
--- a/test-suite/primitive/uint63/head0.v
+++ b/test-suite/primitive/uint63/head0.v
@@ -1,4 +1,4 @@
-Require Import Int63.
+Require Import PrimInt63.
Set Implicit Arguments.
diff --git a/test-suite/primitive/uint63/subcarryc.v b/test-suite/primitive/uint63/subcarryc.v
index e81b6536b2..6a773dde5d 100644
--- a/test-suite/primitive/uint63/subcarryc.v
+++ b/test-suite/primitive/uint63/subcarryc.v
@@ -1,4 +1,4 @@
-Require Import Int63.
+Require Import PrimInt63.
Set Implicit Arguments.
diff --git a/test-suite/primitive/uint63/tail0.v b/test-suite/primitive/uint63/tail0.v
index c9d426087a..1f91e4106c 100644
--- a/test-suite/primitive/uint63/tail0.v
+++ b/test-suite/primitive/uint63/tail0.v
@@ -1,4 +1,4 @@
-Require Import Int63.
+Require Import PrimInt63.
Set Implicit Arguments.
diff --git a/theories/Floats/PrimFloat.v b/theories/Floats/PrimFloat.v
index ed7947aa63..4c818a7e52 100644
--- a/theories/Floats/PrimFloat.v
+++ b/theories/Floats/PrimFloat.v
@@ -8,7 +8,7 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-Require Import Int63 FloatClass.
+Require Import PrimInt63 FloatClass.
(** * Definition of the interface for primitive floating-point arithmetic
diff --git a/theories/Numbers/Cyclic/Abstract/CarryType.v b/theories/Numbers/Cyclic/Abstract/CarryType.v
new file mode 100644
index 0000000000..a21a1c8022
--- /dev/null
+++ b/theories/Numbers/Cyclic/Abstract/CarryType.v
@@ -0,0 +1,18 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
+(************************************************************************)
+
+Set Implicit Arguments.
+
+#[universes(template)]
+Variant carry (A : Type) :=
+| C0 : A -> carry A
+| C1 : A -> carry A.
diff --git a/theories/Numbers/Cyclic/Abstract/DoubleType.v b/theories/Numbers/Cyclic/Abstract/DoubleType.v
index 165f9893ca..e399bcfc0f 100644
--- a/theories/Numbers/Cyclic/Abstract/DoubleType.v
+++ b/theories/Numbers/Cyclic/Abstract/DoubleType.v
@@ -13,15 +13,15 @@
Set Implicit Arguments.
Require Import BinInt.
+Require Import CarryType.
Local Open Scope Z_scope.
Definition base digits := Z.pow 2 (Zpos digits).
Arguments base digits: simpl never.
-#[universes(template)]
-Variant carry (A : Type) :=
-| C0 : A -> carry A
-| C1 : A -> carry A.
+Notation carry := carry (only parsing).
+Notation C0 := C0 (only parsing).
+Notation C1 := C1 (only parsing).
Definition interp_carry {A} (sign:Z)(B:Z)(interp:A -> Z) c :=
match c with
diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v
index dbca2f0947..c469a49903 100644
--- a/theories/Numbers/Cyclic/Int63/Int63.v
+++ b/theories/Numbers/Cyclic/Int63/Int63.v
@@ -17,55 +17,25 @@ Require Import Zpow_facts.
Require Import Zgcd_alt.
Require ZArith.
Import Znumtheory.
-
-Register bool as kernel.ind_bool.
-Register prod as kernel.ind_pair.
-Register carry as kernel.ind_carry.
-Register comparison as kernel.ind_cmp.
+Require Export PrimInt63.
Definition size := 63%nat.
-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 Import 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.
+Notation int := int (only parsing).
+Notation lsl := lsl (only parsing).
+Notation lsr := lsr (only parsing).
+Notation land := land (only parsing).
+Notation lor := lor (only parsing).
+Notation lxor := lxor (only parsing).
+Notation add := add (only parsing).
+Notation sub := sub (only parsing).
+Notation mul := mul (only parsing).
+Notation mulc := mulc (only parsing).
+Notation div := div (only parsing).
+Notation mod := mod (only parsing).
+Notation eqb := eqb (only parsing).
+Notation ltb := ltb (only parsing).
+Notation leb := leb (only parsing).
Local Open Scope int63_scope.
@@ -139,34 +109,29 @@ Register Inline subcarry.
Definition addc_def x y :=
let r := x + y in
if r <? x then C1 r else C0 r.
-(* the same but direct implementation for efficiency *)
-Primitive addc := #int63_addc.
+Notation addc := addc (only parsing).
Definition addcarryc_def x y :=
let r := addcarry x y in
if r <=? x then C1 r else C0 r.
-(* the same but direct implementation for efficiency *)
-Primitive addcarryc := #int63_addcarryc.
+Notation addcarryc := addcarryc (only parsing).
Definition subc_def x y :=
if y <=? x then C0 (x - y) else C1 (x - y).
-(* the same but direct implementation for efficiency *)
-Primitive subc := #int63_subc.
+Notation subc := subc (only parsing).
Definition subcarryc_def x y :=
if y <? x then C0 (x - y - 1) else C1 (x - y - 1).
-(* the same but direct implementation for efficiency *)
-Primitive subcarryc := #int63_subcarryc.
+Notation subcarryc := subcarryc (only parsing).
Definition diveucl_def x y := (x/y, x mod y).
-(* the same but direct implementation for efficiency *)
-Primitive diveucl := #int63_diveucl.
+Notation diveucl := diveucl (only parsing).
-Primitive diveucl_21 := #int63_div21.
+Notation diveucl_21 := diveucl_21 (only parsing).
Definition addmuldiv_def p x y :=
(x << p) lor (y >> (digits - p)).
-Primitive addmuldiv := #int63_addmuldiv.
+Notation addmuldiv := addmuldiv (only parsing).
Module Import Int63NotationsInternalC.
Notation "- x" := (opp x) : int63_scope.
@@ -188,7 +153,7 @@ Definition compare_def x y :=
if x <? y then Lt
else if (x =? y) then Eq else Gt.
-Primitive compare := #int63_compare.
+Notation compare := compare (only parsing).
Import Bool ZArith.
(** Translation to Z *)
@@ -371,8 +336,8 @@ Axiom leb_spec : forall x y, (x <=? y)%int63 = true <-> φ x <= φ y.
(** Exotic operations *)
(** I should add the definition (like for compare) *)
-Primitive head0 := #int63_head0.
-Primitive tail0 := #int63_tail0.
+Notation head0 := head0 (only parsing).
+Notation tail0 := tail0 (only parsing).
(** Axioms on operations which are just short cut *)
@@ -1950,7 +1915,6 @@ Module Export Int63Notations.
Notation "m <= n" := (m <=? n) : int63_scope.
#[deprecated(since="8.13",note="use infix ≤? instead")]
Notation "m ≤ n" := (m <=? n) (at level 70, no associativity) : int63_scope.
- Export Int63NotationsInternalA.
Export Int63NotationsInternalB.
Export Int63NotationsInternalC.
Export Int63NotationsInternalD.
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 05:01:57 +0000