diff options
| author | Hugo Herbelin | 2020-10-09 17:32:44 +0000 |
|---|---|---|
| committer | Hugo Herbelin | 2020-10-16 01:29:19 +0200 |
| commit | 0f403373e6ecc1be806b9c29812f5c9f48c321de (patch) | |
| tree | 5537154ba078467d8932787ed4b07417f9238481 /vernac/comAssumption.ml | |
| parent | 12ea3318943f2a47f45d939aa206acc263a6341d (diff) | |
Fixes/enhancements with local definitions in records.
Fixes implicit arguments from the body of a defined field not taken into account.
Get (a bit) more information for detection of SProp relevance in
implicitly-typed defined field. (It should be done at the very end of
the inference phase, though, because some evars may not yet be
instantiated.)
Diffstat (limited to 'vernac/comAssumption.ml')
| -rw-r--r-- | vernac/comAssumption.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 56f846ebdb..12194ea20c 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -71,7 +71,8 @@ let declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl {CAst.v=name let interp_assumption ~program_mode env sigma impl_env bl c = let flags = { Pretyping.all_no_fail_flags with program_mode } in let sigma, (impls, ((env_bl, ctx), impls1)) = interp_context_evars ~program_mode ~impl_env env sigma bl in - let sigma, (ty, impls2) = interp_type_evars_impls ~flags env sigma ~impls c in + let sigma, (ty, impls2) = interp_type_evars_impls ~flags env_bl sigma ~impls c in + let ty = EConstr.it_mkProd_or_LetIn ty ctx in sigma, ty, impls1@impls2 (* When monomorphic the universe constraints and universe names are |