diff options
| author | Matthieu Sozeau | 2018-10-16 15:58:32 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2018-10-16 15:58:32 +0200 |
| commit | 2917fd2cce3a28da7a28fe6bc8f5a12e480243a2 (patch) | |
| tree | 759efd6deef75742bc620d6156f110338efed964 /pretyping | |
| parent | 096d4dd94ff6d506e7a3785da453c21874611cec (diff) | |
| parent | c70cc62e74341ccda9a67fccdefb03f6d122406c (diff) | |
Merge PR #8059: Simplify code for [Definition := Eval ...]
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) |