diff options
| -rw-r--r-- | vernac/declare.ml | 2 | ||||
| -rw-r--r-- | vernac/declare.mli | 3 |
2 files changed, 5 insertions, 0 deletions
diff --git a/vernac/declare.ml b/vernac/declare.ml index 6a4511ead8..366dd2d026 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -884,3 +884,5 @@ let declare_definition_scheme ~internal ~univs ~role ~name c = let _ = Ind_tables.declare_definition_scheme := declare_definition_scheme let _ = Abstract.declare_abstract := declare_abstract + +let declare_universe_context = DeclareUctx.declare_universe_context diff --git a/vernac/declare.mli b/vernac/declare.mli index a551c621c4..e23e148ddc 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -279,3 +279,6 @@ val build_constant_by_tactic : EConstr.types -> unit Proofview.tactic -> Evd.side_effects proof_entry * bool * UState.t + +val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit +[@@ocaml.deprecated "Use DeclareUctx.declare_universe_context"] |