From 1bc1cba7a759a285131a3ed6ea8979716700b856 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 20 Sep 2016 17:13:27 +0200
Subject: 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.
---
 stm/lemmas.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'stm')

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)
-- 
cgit v1.2.3