diff options
| author |  Matej Kosik <matej.kosik@inria.fr> | 2016-10-25 15:16:42 +0200 |
|---|---|---|
| committer | Matej Kosik <matej.kosik@inria.fr> | 2016-10-26 10:55:32 +0200 |
| commit | 36b75df8ad9b118648ff0c295a097e71775b7656 (patch) | |
| tree | 91852ef4f9db3f4a5c9fa67e8a216c86c97e5415 /kernel | |
| parent | 68dfa4701d7636728270dfd8f33133627486204b (diff) | |
COMMENT: Declarations.constant_def
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/declarations.mli | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli index fe2fa6d7f..7821ea20f 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -58,10 +58,11 @@ type projection_body = { proj_body : constr; (* For compatibility with VMs only, the match version *) } +(* Global declarations (i.e. constants) can be either: *) type constant_def = - | Undef of inline - | Def of constr Mod_subst.substituted - | OpaqueDef of Opaqueproof.opaque + | Undef of inline (** a global assumption *) + | Def of constr Mod_subst.substituted (** or a transparent global definition *) + | OpaqueDef of Opaqueproof.opaque (** or an opaque global definition *) type constant_universes = Univ.universe_context |