diff options
| author | Emilio Jesus Gallego Arias | 2020-04-20 03:13:08 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-04-21 08:39:13 +0200 |
| commit | 8de0fcaa08c82ece8874606e8fa1954d860bd88e (patch) | |
| tree | 8cf8eef8df0f9fd91408b9648317d2c96e63cfa6 | |
| parent | 579d192cc4c21d3a2a325dc501181d262040482f (diff) | |
[declare] [compat] Add alias for deprecated function
| -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"] |