diff options
| author | Pierre-Marie Pédrot | 2019-02-18 13:09:14 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-18 13:09:14 +0100 |
| commit | a59574c8eb4bdda60e4bdd6197e8a32574985588 (patch) | |
| tree | e15e1a0f78d23cd263726d725c93a5e6ce453465 /kernel/cbytegen.ml | |
| parent | f8d6c322783577b31cf55f8b55568ac56104202b (diff) | |
| parent | a9f0fd89cf3bb4b728eb451572a96f8599211380 (diff) | |
Merge PR #9439: Separate variance and universe fields in inductives.
Ack-by: ppedrot
Diffstat (limited to 'kernel/cbytegen.ml')
| -rw-r--r-- | kernel/cbytegen.ml | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index b95a940c14..718584b3d4 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -881,11 +881,7 @@ let compile_constant_body ~fail_on_error env univs = function | Undef _ | OpaqueDef _ | Primitive _ -> Some BCconstant | Def sb -> let body = Mod_subst.force_constr sb in - let instance_size = - match univs with - | Monomorphic_const _ -> 0 - | Polymorphic_const univ -> Univ.AUContext.size univ - in + let instance_size = Univ.AUContext.size (Declareops.universes_context univs) in match kind body with | Const (kn',u) when is_univ_copy instance_size u -> (* we use the canonical name of the constant*) |