diff options
Diffstat (limited to 'pretyping/nativenorm.ml')
| -rw-r--r-- | pretyping/nativenorm.ml | 5 |
1 files changed, 3 insertions, 2 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 | _ -> |