diff options
| author | Matthieu Sozeau | 2014-08-03 23:19:56 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-08-03 23:39:02 +0200 |
| commit | ead5d80dff08f97998e81acfb2562dde741a26af (patch) | |
| tree | 7b5ad21993d0c1625f6609eba0e385378ca43faf /toplevel | |
| parent | ef72be87579be34e9454fe1f785ff36a9c25246c (diff) | |
Fix infer conv using the wrong universe conversion flexibility information
for constants that are not unfolded during conversion.
Fix discharge of polymorphic section variables over inductive types.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/discharge.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 971ae70d86..9de0edea81 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -101,6 +101,7 @@ let process_inductive (sechyps,abs_ctx) modlist mib = mib.mind_packets in let sechyps' = map_named_context (expmod_constr modlist) sechyps in let (params',inds') = abstract_inductive sechyps' nparams inds in + let abs_ctx = Univ.instantiate_univ_context abs_ctx in let univs = Univ.UContext.union abs_ctx univs in let record = match mib.mind_record with | None -> None |