diff options
| author | Pierre-Marie Pédrot | 2019-04-11 12:07:00 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-04-11 12:07:00 +0200 |
| commit | 38b86f40b3e2c6ce0ea77c94cf0c48efbf7c9f13 (patch) | |
| tree | 73c615fe6e2853d5879eebbd034d18bdf8fd686b /vernac/comAssumption.mli | |
| parent | 36c15766a9295d980d142da0e42aebf1309f4eb4 (diff) | |
| parent | 9fe0932a7b04eecea35f98bc2b38beebb64d476a (diff) | |
Merge PR #9909: Remove all but one call to `Global` in the pretyper
Ack-by: ejgallego
Reviewed-by: gares
Ack-by: maximedenes
Ack-by: ppedrot
Diffstat (limited to 'vernac/comAssumption.mli')
| -rw-r--r-- | vernac/comAssumption.mli | 20 |
1 files changed, 11 insertions, 9 deletions
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index 32914cc11b..7c64317b70 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -9,8 +9,6 @@ (************************************************************************) open Names -open Constr -open Entries open Vernacexpr open Constrexpr open Decl_kinds @@ -25,19 +23,13 @@ val do_assumptions -> (ident_decl list * constr_expr) with_coercion list -> bool -(************************************************************************) -(** Internal API *) -(************************************************************************) - -(** Exported for Classes *) - (** 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 -> assumption_kind - -> types in_universes_entry + -> Constr.types Entries.in_universes_entry -> UnivNames.universe_binders -> Impargs.manual_implicits -> bool (** implicit *) @@ -45,4 +37,14 @@ val declare_assumption -> variable CAst.t -> GlobRef.t * Univ.Instance.t * bool +(** Context command *) + +(** 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 + -> local_binder_expr list + -> bool + val do_primitive : lident -> CPrimitives.op_or_type -> constr_expr option -> unit |