diff options
| author | Pierre-Marie Pédrot | 2021-01-19 13:45:27 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-19 13:45:27 +0100 |
| commit | 071c50e9c2755e93766e5fb047b0a9065934e8fe (patch) | |
| tree | 1c702aafeebc10843c76ba992658000d9b6e864e /test-suite/output/Int63Syntax.v | |
| parent | a85d8cb68f53667d13ae0b5210b5e3dcc3fd8aa4 (diff) | |
| parent | 7df37822980666c51109205dca8df99f3b81c4fb (diff) | |
Merge PR #13699: Fix #13579 (hnf on primitives raises an anomaly)
Ack-by: SkySkimmer
Reviewed-by: ppedrot
Diffstat (limited to 'test-suite/output/Int63Syntax.v')
| -rw-r--r-- | test-suite/output/Int63Syntax.v | 15 |
1 files changed, 15 insertions, 0 deletions
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. |