diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-13 07:18:22 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-17 10:56:04 +0100 |
commit | 7a5688f6e2421a706c16e23e445d42f39a82e74b (patch) | |
tree | 4dfc0054afb151a93e185ab21a51748e4b2086ea /vernac/comAssumption.mli | |
parent | 53f5cc210da4debd5264d6d8651a76281b0b4256 (diff) |
[vernac] Split `command.ml` into separate files.
Over the time, `Command` grew organically and it has become now one of
the most complex files in the codebase; however, its functionality is
well separated into 4 key components that have little to do with each
other.
We thus split the file, and also document the interfaces. Some parts
of `Command` export tricky internals to use by other plugins, and it
is common that plugin writers tend to get confused, so we are more
explicit about these parts now.
This patch depends on #6413.
Diffstat (limited to 'vernac/comAssumption.mli')
-rw-r--r-- | vernac/comAssumption.mli | 34 |
1 files changed, 34 insertions, 0 deletions
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli new file mode 100644 index 000000000..2fa156abd --- /dev/null +++ b/vernac/comAssumption.mli @@ -0,0 +1,34 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Constr +open Entries +open Globnames +open Vernacexpr +open Constrexpr +open Decl_kinds + +(** {6 Parameters/Assumptions} *) + +val do_assumptions : locality * polymorphic * assumption_object_kind -> + Vernacexpr.inline -> (Vernacexpr.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 : coercion_flag -> assumption_kind -> + types in_constant_universes_entry -> + Universes.universe_binders -> Impargs.manual_implicits -> + bool (** implicit *) -> Vernacexpr.inline -> variable Loc.located -> + global_reference * Univ.Instance.t * bool |