diff options
| author | Pierre Roux | 2020-10-26 14:43:05 +0100 |
|---|---|---|
| committer | Pierre Roux | 2020-12-02 09:26:53 +0100 |
| commit | 853b838681db635f51fc3c7ba3dfe26bc6712d72 (patch) | |
| tree | 0b23386f296313f4fae2a0db293e1f441834f7e4 /theories/Numbers/Cyclic/Abstract | |
| parent | 9e7b0f9f248a1fae8e5681815bd621f182696c4f (diff) | |
Put all Int63 primitives in a separate file
Following a request from Pierre-Marie Pédrot in #13258
Diffstat (limited to 'theories/Numbers/Cyclic/Abstract')
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/CarryType.v | 18 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/DoubleType.v | 8 |
2 files changed, 22 insertions, 4 deletions
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 |