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 /test-suite/primitive | |
| parent | 9e7b0f9f248a1fae8e5681815bd621f182696c4f (diff) | |
Put all Int63 primitives in a separate file
Following a request from Pierre-Marie Pédrot in #13258
Diffstat (limited to 'test-suite/primitive')
| -rw-r--r-- | test-suite/primitive/uint63/addcarryc.v | 2 | ||||
| -rw-r--r-- | test-suite/primitive/uint63/addmuldiv.v | 2 | ||||
| -rw-r--r-- | test-suite/primitive/uint63/diveucl.v | 2 | ||||
| -rw-r--r-- | test-suite/primitive/uint63/head0.v | 2 | ||||
| -rw-r--r-- | test-suite/primitive/uint63/subcarryc.v | 2 | ||||
| -rw-r--r-- | test-suite/primitive/uint63/tail0.v | 2 |
6 files changed, 6 insertions, 6 deletions
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. |