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.
---
 interp/notation_ops.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/notation_ops.mli')

diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index 854e222e30..6428ccab66 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -48,7 +48,7 @@ val glob_constr_of_notation_constr : Loc.t -> notation_constr -> glob_constr
 exception No_match
 
 type glob_decl2 =
-    (name, cases_pattern) Util.union * Decl_kinds.binding_kind *
+    (name, cases_pattern) Util.union * Decl_kinds.implicit_status *
       glob_constr option * glob_constr
 val match_notation_constr : bool -> glob_constr -> interpretation ->
       (glob_constr * subscopes) list * (glob_constr list * subscopes) list *
-- 
cgit v1.2.3