diff options
| -rw-r--r-- | pretyping/nativenorm.ml | 5 | ||||
| -rw-r--r-- | pretyping/vnorm.ml | 13 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_7631.v | 6 |
3 files changed, 16 insertions, 8 deletions
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 92e412a537..55ff91327a 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -135,8 +135,9 @@ let construct_of_constr_notnative const env tag (mind, _ as ind) u allargs = let construct_of_constr const env sigma tag typ = - let t, l = app_type env typ in - match EConstr.kind_upto sigma t with + let typ = Reductionops.clos_whd_flags CClosure.all env sigma (EConstr.of_constr typ) in + let t, l = decompose_appvect (EConstr.Unsafe.to_constr typ) in + match Constr.kind t with | Ind (ind,u) -> construct_of_constr_notnative const env tag ind u l | _ -> 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 diff --git a/test-suite/bugs/closed/bug_7631.v b/test-suite/bugs/closed/bug_7631.v index 93aeb83e28..14ab4de9b7 100644 --- a/test-suite/bugs/closed/bug_7631.v +++ b/test-suite/bugs/closed/bug_7631.v @@ -21,3 +21,9 @@ Definition bar (x := foo) := Eval native_compute in x. Definition barvm (x := foo) := Eval vm_compute in x. End RelContext. + +Definition bar (t:=_) (x := true : t) := Eval native_compute in x. +Definition barvm (t:=_) (x := true : t) := Eval vm_compute in x. + +Definition baz (z:nat) (t:=_ z) (x := true : t) := Eval native_compute in x. +Definition bazvm (z:nat) (t:=_ z) (x := true : t) := Eval vm_compute in x. |