From 60fe31e2424383abaa6c7a86aa65a76bbbc7eff3 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 13 Jul 2018 15:08:17 +0200
Subject: Fix nativenorm when an evar is in the wrong place.

See commit [Simplify code for [Definition := Eval ...]] which without
this breaks test suite 7631.v
---
 test-suite/bugs/closed/bug_7631.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_7631.v b/test-suite/bugs/closed/bug_7631.v
index 34eb8b8676..93aeb83e28 100644
--- a/test-suite/bugs/closed/bug_7631.v
+++ b/test-suite/bugs/closed/bug_7631.v
@@ -7,6 +7,7 @@ Section Foo.
 Let bar := foo.
 
 Eval native_compute in bar.
+Eval vm_compute in bar.
 
 End Foo.
 
@@ -17,5 +18,6 @@ Module RelContext.
 Definition foo := true.
 
 Definition bar (x := foo) := Eval native_compute in x.
+Definition barvm (x := foo) := Eval vm_compute in x.
 
 End RelContext.
-- 
cgit v1.2.3