diff options
| author | Maxime Dénès | 2017-11-28 11:10:56 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-28 11:10:56 +0100 |
| commit | 24adb2ee00b860f4550d05bd38dde4a284bcd7bc (patch) | |
| tree | 2c32fc1aa8724ab4685c6a9a0e568eb49132d9f5 /kernel/declareops.ml | |
| parent | ddfca160f14eba979bcaa238da4c91e4e445f37b (diff) | |
| parent | d1d18519cfcf0787203b73fb050f76355ff26adf (diff) | |
Merge PR #1033: Universe binder improvements
Diffstat (limited to 'kernel/declareops.ml')
| -rw-r--r-- | kernel/declareops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/declareops.ml b/kernel/declareops.ml index f5c26b33d6..d8768a0fc5 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -126,7 +126,7 @@ let hcons_const_def = function let hcons_const_universes cbu = match cbu with | Monomorphic_const ctx -> - Monomorphic_const (Univ.hcons_universe_context ctx) + Monomorphic_const (Univ.hcons_universe_context_set ctx) | Polymorphic_const ctx -> Polymorphic_const (Univ.hcons_abstract_universe_context ctx) @@ -274,7 +274,7 @@ let hcons_mind_packet oib = let hcons_mind_universes miu = match miu with - | Monomorphic_ind ctx -> Monomorphic_ind (Univ.hcons_universe_context ctx) + | Monomorphic_ind ctx -> Monomorphic_ind (Univ.hcons_universe_context_set ctx) | Polymorphic_ind ctx -> Polymorphic_ind (Univ.hcons_abstract_universe_context ctx) | Cumulative_ind cui -> Cumulative_ind (Univ.hcons_abstract_cumulativity_info cui) |