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

2 files changed, 8 insertions, 6 deletions

diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 20185363e6..022c383f60 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -132,15 +132,15 @@ let construct_of_constr_notnative const env tag (mind, _ as ind) u allargs =
   (mkApp(mkConstructU((ind,i),u), params), ctyp)
  
 
-let construct_of_constr const env tag typ =
+let construct_of_constr const env sigma tag typ =
   let t, l = app_type env typ in
-  match kind t with
+  match EConstr.kind_upto sigma t with
   | Ind (ind,u) -> 
       construct_of_constr_notnative const env tag ind u l
   | _ -> assert false
 
-let construct_of_constr_const env tag typ = 
-  fst (construct_of_constr true env tag typ)
+let construct_of_constr_const env sigma tag typ =
+  fst (construct_of_constr true env sigma tag typ)
 
 let construct_of_constr_block = construct_of_constr false
 
@@ -207,9 +207,9 @@ let rec nf_val env sigma v typ =
       let env = push_rel (LocalAssum (name,dom)) env in
       let body = nf_val env sigma (f (mk_rel_accu lvl)) codom in
       mkLambda(name,dom,body)
-  | Vconst n -> construct_of_constr_const env n typ
+  | Vconst n -> construct_of_constr_const env sigma n typ
   | Vblock b ->
-      let capp,ctyp = construct_of_constr_block env (block_tag b) typ in
+      let capp,ctyp = construct_of_constr_block env sigma (block_tag b) typ in
       let args = nf_bargs env sigma b ctyp in
       mkApp(capp,args)
 
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.