diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-12-05 12:56:11 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-05 12:56:11 +0100 |
| commit | 2c5e81e3bc6ec17d253aeedd1b2bf4ccd3b81933 (patch) | |
| tree | 1e8d3db28d8d19b575e9e555f6ce379960c842c1 /vernac/classes.ml | |
| parent | d403b2200ef32afd1eb1087a1f0ef2e6b8bb93f6 (diff) | |
| parent | 17b620f8bdf47a744d24513dcaef720d9160d443 (diff) | |
Merge PR #890: Global universe declarations
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index b80741269..cb1d2f7c7 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -126,7 +126,7 @@ let declare_instance_constant k info global imps ?hook id decl poly evm term ter let cdecl = (DefinitionEntry entry, kind) in let kn = Declare.declare_constant id cdecl in Declare.definition_message id; - Universes.register_universe_binders (ConstRef kn) (Evd.universe_binders evm); + Declare.declare_univ_binders (ConstRef kn) (Evd.universe_binders evm); instance_hook k info global imps ?hook (ConstRef kn); id @@ -208,7 +208,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) (ParameterEntry (None,(termtype,univs),None), Decl_kinds.IsAssumption Decl_kinds.Logical) in - Universes.register_universe_binders (ConstRef cst) (Evd.universe_binders !evars); + Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders !evars); instance_hook k pri global imps ?hook (ConstRef cst); id end else ( |