diff options
| author | Emilio Jesus Gallego Arias | 2019-05-21 16:48:03 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-05-21 16:48:03 +0200 |
| commit | e9a5fe993ba36e22316ac9f6ef0564f38a3eb4f9 (patch) | |
| tree | 0ffb42301743171b24d6bb0c4205eba78e889e50 /vernac/comAssumption.mli | |
| parent | 0aa9a5407874332dfa31f1a0f73d2dc91e95fb39 (diff) | |
| parent | f6751f5e8aae4f37d302f700d2f5f2e9fba73a1e (diff) | |
Merge PR #10188: Remove definition-not-visible warning
Reviewed-by: gares
Diffstat (limited to 'vernac/comAssumption.mli')
| -rw-r--r-- | vernac/comAssumption.mli | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index 7c64317b70..8f37bc0ba4 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -16,8 +16,7 @@ open Decl_kinds (** {6 Parameters/Assumptions} *) val do_assumptions - : pstate:Proof_global.t option - -> program_mode:bool + : program_mode:bool -> locality * polymorphic * assumption_object_kind -> Declaremods.inline -> (ident_decl list * constr_expr) with_coercion list @@ -26,8 +25,7 @@ val do_assumptions (** returns [false] if the assumption is neither local to a section, nor in a module type and meant to be instantiated. *) val declare_assumption - : pstate:Proof_global.t option - -> coercion_flag + : coercion_flag -> assumption_kind -> Constr.types Entries.in_universes_entry -> UnivNames.universe_binders @@ -42,8 +40,7 @@ val declare_assumption (** returns [false] if, for lack of section, it declares an assumption (unless in a module type). *) val context - : pstate:Proof_global.t option - -> Decl_kinds.polymorphic + : Decl_kinds.polymorphic -> local_binder_expr list -> bool |