diff options
| author | Guillaume Melquiond | 2021-02-23 17:51:07 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2021-02-24 00:08:09 +0100 |
| commit | b31c4fa57eac8162ad6b6e03f75b13afd9b76db7 (patch) | |
| tree | e379b0769b89831d4756733cc068b2a2ff3da206 /pretyping/vnorm.ml | |
| parent | f89f0eb4717b64f10bdd0a0edc9e93b949bcb33d (diff) | |
Use Reductionops.clos_whd_flags in vm_compute and native_compute.
Diffstat (limited to 'pretyping/vnorm.ml')
| -rw-r--r-- | pretyping/vnorm.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 5622bd357a..9939764069 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -78,8 +78,9 @@ let type_constructor mind mib u (ctx, typ) params = -let construct_of_constr const env tag typ = - let (t, allargs) = decompose_appvect (whd_all env typ) in +let construct_of_constr const env sigma tag typ = + let typ = Reductionops.clos_whd_flags CClosure.all env sigma (EConstr.of_constr typ) in + let t, allargs = decompose_appvect (EConstr.Unsafe.to_constr typ) in match Constr.kind t with | Ind ((mind,_ as ind), u as indu) -> let mib,mip = lookup_mind_specif env ind in @@ -92,8 +93,8 @@ let construct_of_constr const env tag typ = assert (Constr.equal t (Typeops.type_of_int env)); (mkInt (Uint63.of_int tag), t) -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 @@ -156,7 +157,7 @@ and nf_whd env sigma whd typ = let _, args = nf_args env sigma vargs t in mkApp(cfd,args) | Vconstr_const n -> - construct_of_constr_const env n typ + construct_of_constr_const env sigma n typ | Vconstr_block b -> let tag = btag b in let (tag,ofs) = @@ -165,7 +166,7 @@ and nf_whd env sigma whd typ = | Vconstr_const tag -> (tag+Obj.last_non_constant_constructor_tag, 1) | _ -> assert false else (tag, 0) in - let capp,ctyp = construct_of_constr_block env tag typ in + let capp,ctyp = construct_of_constr_block env sigma tag typ in let args = nf_bargs env sigma b ofs ctyp in mkApp(capp,args) | Vint64 i -> i |> Uint63.of_int64 |> mkInt |