diff options
| -rw-r--r-- | doc/dune | 2 | ||||
| -rw-r--r-- | vernac/comAssumption.ml | 15 | ||||
| -rw-r--r-- | vernac/comAssumption.mli | 16 |
3 files changed, 1 insertions, 32 deletions
@@ -14,7 +14,7 @@ unreleased.rst (env_var SPHINXWARNOPT)) (action - (run env COQLIB=%{project_root} sphinx-build -j4 %{env:SPHINXWARNOPT=-W} -b html -d sphinx_build/doctrees sphinx sphinx_build/html))) + (run env COQLIB=%{project_root} sphinx-build %{env:SPHINXWARNOPT=-W} -b html -d sphinx_build/doctrees sphinx sphinx_build/html))) (alias (name refman-html) 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 diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index ae9edefcac..f5192fc696 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -50,19 +50,3 @@ val context : poly:bool -> local_binder_expr list -> unit - -(** Deprecated *) -val declare_assumption - : coercion_flag - -> poly:bool - -> scope:DeclareDef.locality - -> kind:Decls.assumption_object_kind - -> Constr.types - -> Entries.universes_entry - -> UnivNames.universe_binders - -> Impargs.manual_implicits - -> Glob_term.binding_kind - -> Declaremods.inline - -> variable CAst.t - -> GlobRef.t * Univ.Instance.t -[@@ocaml.deprecated "Use declare_variable or declare_axiom instead."] |