diff options
| author | Gaëtan Gilbert | 2018-07-13 15:08:17 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-10-09 13:26:21 +0200 |
| commit | 60fe31e2424383abaa6c7a86aa65a76bbbc7eff3 (patch) | |
| tree | 1ab4ff0993b7562e490b0c85c5269d94e24d8001 /pretyping | |
| parent | 59de2827b63b5bc475452bef385a2149a10a631c (diff) | |
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
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/nativenorm.ml | 12 |
1 files changed, 6 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) |