diff options
| author | Pierre-Marie Pédrot | 2019-02-04 17:22:36 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-04 17:22:36 +0100 |
| commit | c70412ec8b0bb34b7a5607c07d34607a147d834c (patch) | |
| tree | 0cc6cd76a8f70dfd2f5b55b0db96db4de2ff07a2 /test-suite/output/Int31Syntax.v | |
| parent | 720ee2730684cc289cef588482323d177e0bea59 (diff) | |
| parent | 191e253d1d1ebd6c76c63b3d83f4228e46196a6e (diff) | |
Merge PR #6914: Primitive integers
Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Ack-by: maximedenes
Ack-by: ppedrot
Diffstat (limited to 'test-suite/output/Int31Syntax.v')
| -rw-r--r-- | test-suite/output/Int31Syntax.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/test-suite/output/Int31Syntax.v b/test-suite/output/Int31Syntax.v index 83be3b976b..48889a26ef 100644 --- a/test-suite/output/Int31Syntax.v +++ b/test-suite/output/Int31Syntax.v @@ -3,11 +3,12 @@ Require Import Int31 Cyclic31. Open Scope int31_scope. Check I31. (* Would be nice to have I31 : digits->digits->...->int31 For the moment, I31 : digits31 int31, which is better - than (fix nfun .....) size int31 *) + than (fix nfun .....) size int31 *) Check 2. Check 1000000000000000000. (* = 660865024, after modulo 2^31 *) Check (add31 2 2). Check (2+2). Eval vm_compute in 2+2. Eval vm_compute in 65675757 * 565675998. +Fail Check -1. Close Scope int31_scope. |