diff options
| author | Maxime Dénès | 2016-09-20 17:13:27 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-09-20 17:18:37 +0200 |
| commit | 1bc1cba7a759a285131a3ed6ea8979716700b856 (patch) | |
| tree | 25202d41487d954621fb4bc42affd75bbae662cb /toplevel | |
| parent | aa29c92dfa395e2f369e81bd72cef482cdf90c65 (diff) | |
Rename Decl_kinds.binding_kind into Decls_kind.implicit_status.
The new name makes it more obvious what is meant here by "kind". We leave
Decl_kinds.binding_kind as a deprecated alias for plugin
compatibility.
We also replace bool with implicit_status in a few places in the
codebase.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 2 | ||||
| -rw-r--r-- | toplevel/command.mli | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 40c65b56fa..7bb016d34a 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -230,7 +230,7 @@ let declare_assumption is_coe assumption_kind (c,ctx) pl imps impl nl (_,ident) | Discharge when Lib.sections_are_opened () -> let entry = SectionLocalAssum { type_context = (c,ctx); polymorphic; - binding_kind = impl } + implicit_status = impl } in let decl = (Lib.cwd(), entry, IsAssumption kind) in let _ = declare_variable ident decl in diff --git a/toplevel/command.mli b/toplevel/command.mli index 2ae4cddd06..f0651a98c8 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -55,7 +55,7 @@ val do_definition : Id.t -> definition_kind -> lident list option -> val declare_assumption : coercion_flag -> assumption_kind -> types Univ.in_universe_context_set -> Universes.universe_binders -> Impargs.manual_implicits -> - binding_kind -> Vernacexpr.inline -> variable Loc.located -> + implicit_status -> Vernacexpr.inline -> variable Loc.located -> global_reference * Univ.Instance.t * bool val do_assumptions : assumption_kind -> |