diff options
| author | Emilio Jesus Gallego Arias | 2020-06-03 16:34:39 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-03 17:33:25 +0200 |
| commit | 6fe12fdac4acee36c99ea780d260ce5a9756cb1d (patch) | |
| tree | 9e3016023ed13df51988a84e6f1f8b26d4b0584d /vernac/declare.mli | |
| parent | 5ea6ef71681770a98edc5ede8614d2cf0bd48554 (diff) | |
[declare] Hide internals of variable declaration entries.
In particular this avoids exposing `Evd.side_effects proof_entry` in
the API.
Diffstat (limited to 'vernac/declare.mli')
| -rw-r--r-- | vernac/declare.mli | 10 |
1 files changed, 2 insertions, 8 deletions
diff --git a/vernac/declare.mli b/vernac/declare.mli index 5339f4702b..ef4f8c4825 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -119,13 +119,6 @@ val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Proof.t (** XXX: This is an internal, low-level API and could become scheduled for removal from the public API, use higher-level declare APIs instead *) -type variable_declaration = - | SectionLocalDef of Evd.side_effects proof_entry - | SectionLocalAssum of { typ:types; impl:Glob_term.binding_kind; } - -(** XXX: This is an internal, low-level API and could become scheduled - for removal from the public API, use higher-level declare APIs - instead *) type 'a constant_entry = | DefinitionEntry of 'a proof_entry | ParameterEntry of parameter_entry @@ -134,7 +127,8 @@ type 'a constant_entry = val declare_variable : name:variable -> kind:Decls.logical_kind - -> variable_declaration + -> typ:types + -> impl:Glob_term.binding_kind -> unit (** Declaration of global constructions |