From f724ed1e270eb48060a510ff99219227c342ad6c Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 31 Dec 2020 18:08:29 +0100
Subject: Fix #13579 (hnf on primitives raises an anomaly)

Also works for simpl.
---
 test-suite/output/Int63Syntax.v | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

(limited to 'test-suite/output/Int63Syntax.v')

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.
-- 
cgit v1.2.3