diff options
| author | Emilio Jesus Gallego Arias | 2019-10-30 17:55:27 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-25 15:34:22 -0500 |
| commit | fda9bdb09a2f2f7b98351e047ae43f097b428902 (patch) | |
| tree | bd42dbec8e24093b071db676b66188aca0424da6 /vernac/comAssumption.ml | |
| parent | fe1335eb350c305142bf4be57c681891515a5dac (diff) | |
[vernac] Remove deprecated function.
Diffstat (limited to 'vernac/comAssumption.ml')
| -rw-r--r-- | vernac/comAssumption.ml | 15 |
1 files changed, 0 insertions, 15 deletions
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index d97bf6724c..2e9f0283ca 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -277,18 +277,3 @@ let context ~poly l = if Global.sections_are_opened () then context_insection sigma ~poly ctx else context_nosection sigma ~poly ctx - -(* Deprecated *) -let declare_assumption is_coe ~poly ~scope ~kind typ univs pl imps impl nl name = -let open DeclareDef in -match scope with -| Discharge -> - let univs = match univs with - | Monomorphic_entry univs -> univs - | Polymorphic_entry (_, univs) -> Univ.ContextSet.of_context univs - in - let () = Declare.declare_universe_context ~poly univs in - declare_variable is_coe ~kind typ imps impl name; - GlobRef.VarRef name.CAst.v, Univ.Instance.empty -| Global local -> - declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl name |