From b31c4fa57eac8162ad6b6e03f75b13afd9b76db7 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 23 Feb 2021 17:51:07 +0100
Subject: Use Reductionops.clos_whd_flags in vm_compute and native_compute.

---
 test-suite/bugs/closed/bug_7631.v | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_7631.v b/test-suite/bugs/closed/bug_7631.v
index 93aeb83e28..14ab4de9b7 100644
--- a/test-suite/bugs/closed/bug_7631.v
+++ b/test-suite/bugs/closed/bug_7631.v
@@ -21,3 +21,9 @@ Definition bar (x := foo) := Eval native_compute in x.
 Definition barvm (x := foo) := Eval vm_compute in x.
 
 End RelContext.
+
+Definition bar (t:=_) (x := true : t) := Eval native_compute in x.
+Definition barvm (t:=_) (x := true : t) := Eval vm_compute in x.
+
+Definition baz (z:nat) (t:=_ z) (x := true : t) := Eval native_compute in x.
+Definition bazvm (z:nat) (t:=_ z) (x := true : t) := Eval vm_compute in x.
-- 
cgit v1.2.3