diff options
| author | Pierre Roux | 2020-12-31 18:08:29 +0100 |
|---|---|---|
| committer | Pierre Roux | 2021-01-18 12:09:11 +0100 |
| commit | f724ed1e270eb48060a510ff99219227c342ad6c (patch) | |
| tree | 0552f45d72d5efa46ba19762ca4259899792af2c /test-suite | |
| parent | 1b0f76026a553bcd76efb2bf99048235ad847ada (diff) | |
Fix #13579 (hnf on primitives raises an anomaly)
Also works for simpl.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Int63Syntax.out | 18 | ||||
| -rw-r--r-- | test-suite/output/Int63Syntax.v | 15 |
2 files changed, 33 insertions, 0 deletions
diff --git a/test-suite/output/Int63Syntax.out b/test-suite/output/Int63Syntax.out index ca8e1b58a8..7ca4de1e46 100644 --- a/test-suite/output/Int63Syntax.out +++ b/test-suite/output/Int63Syntax.out @@ -56,3 +56,21 @@ t = 2%i63 : int = 37151199385380486 : int + = 4 + : int + = 4 + : int + = 4 + : int + = add + : int -> int -> int + = 12 + : int + = 12 + : int + = 12 + : int + = 3 + x + : int + = 1 + 2 + x + : int diff --git a/test-suite/output/Int63Syntax.v b/test-suite/output/Int63Syntax.v index 6f1046f7a5..50910264f2 100644 --- a/test-suite/output/Int63Syntax.v +++ b/test-suite/output/Int63Syntax.v @@ -40,3 +40,18 @@ Open Scope int63_scope. Check (2+2). Eval vm_compute in 2+2. Eval vm_compute in 65675757 * 565675998. + +Eval simpl in 2+2. +Eval hnf in 2+2. +Eval cbn in 2+2. +Eval hnf in PrimInt63.add. + +Eval simpl in (2 * 3) + (2 * 3). +Eval hnf in (2 * 3) + (2 * 3). +Eval cbn in (2 * 3) + (2 * 3). + +Section TestNoSimpl. +Variable x : int. +Eval simpl in 1 + 2 + x. +Eval hnf in 1 + 2 + x. +End TestNoSimpl. |