diff options
Diffstat (limited to 'vernac/comAssumption.mli')
| -rw-r--r-- | vernac/comAssumption.mli | 37 |
1 files changed, 28 insertions, 9 deletions
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index 44db47e1cc..ae9edefcac 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -23,27 +23,46 @@ val do_assumptions -> (ident_decl list * constr_expr) with_coercion list -> unit -(** returns [false] if the assumption is neither local to a section, - nor in a module type and meant to be instantiated. *) -val declare_assumption +val declare_variable : 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 + -> variable CAst.t + -> unit + +val declare_axiom + : coercion_flag + -> poly:bool + -> local:Declare.import_status + -> kind:Decls.assumption_object_kind + -> Constr.types + -> Entries.universes_entry * UnivNames.universe_binders + -> Impargs.manual_implicits -> Declaremods.inline -> variable CAst.t -> GlobRef.t * Univ.Instance.t (** Context command *) -(** returns [false] if, for lack of section, it declares an assumption - (unless in a module type). *) 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."] |