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 /stm | |
| 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 'stm')
| -rw-r--r-- | stm/lemmas.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 004dd68017..b1b8aa2889 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -241,7 +241,7 @@ let save_remaining_recthms { locality; polymorphic; object_kind } let k = IsAssumption Conjectural in let c = SectionLocalAssum { type_context = (t_i,ctx); polymorphic; - binding_kind = impl } + implicit_status = impl } in let _ = declare_variable id (Lib.cwd(),c,k) in (Discharge, VarRef id,imps) |