From aa29c92dfa395e2f369e81bd72cef482cdf90c65 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 20 Sep 2016 09:11:09 +0200
Subject: Stylistic improvements in intf/decl_kinds.mli.

We get rid of tuples containing booleans (typically for universe
polymorphism) by replacing them with records.

The previously common idom:

if pi2 kind (* polymorphic *) then ... else ...

becomes:

if kind.polymorphic then ... else ...

To make the construction and destruction of these records lightweight,
the labels of boolean arguments for universe polymorphism are now
usually also called "polymorphic".
---
 intf/decl_kinds.mli | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

(limited to 'intf')

diff --git a/intf/decl_kinds.mli b/intf/decl_kinds.mli
index 6a4e188337..29972f2f46 100644
--- a/intf/decl_kinds.mli
+++ b/intf/decl_kinds.mli
@@ -49,9 +49,13 @@ type assumption_object_kind = Definitional | Logical | Conjectural
    Logical      |  Hypothesis | Axiom
 
 *)
-type assumption_kind = locality * polymorphic * assumption_object_kind
+type 'a declaration_kind = { locality : locality;
+                             polymorphic : bool;
+                             object_kind : 'a }
 
-type definition_kind = locality * polymorphic * definition_object_kind
+type assumption_kind = assumption_object_kind declaration_kind
+
+type definition_kind = definition_object_kind declaration_kind
 
 (** Kinds used in proofs *)
 
@@ -59,7 +63,7 @@ type goal_object_kind =
   | DefinitionBody of definition_object_kind
   | Proof of theorem_kind
 
-type goal_kind = locality * polymorphic * goal_object_kind
+type goal_kind = goal_object_kind declaration_kind
 
 (** Kinds used in library *)
 
-- 
cgit v1.2.3


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.
---
 intf/constrexpr.mli | 8 ++++----
 intf/decl_kinds.mli | 5 ++++-
 intf/glob_term.mli  | 6 +++---
 3 files changed, 11 insertions(+), 8 deletions(-)

(limited to 'intf')

diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index 0cbb29575d..e494b2f81f 100644
--- a/intf/constrexpr.mli
+++ b/intf/constrexpr.mli
@@ -23,8 +23,8 @@ type explicitation =
   | ExplByName of Id.t
 
 type binder_kind =
-  | Default of binding_kind
-  | Generalized of binding_kind * binding_kind * bool
+  | Default of implicit_status
+  | Generalized of implicit_status * implicit_status * bool
       (** Inner binding, outer bindings, typeclass-specific flag
 	 for implicit generalization of superclasses *)
 
@@ -95,7 +95,7 @@ and constr_expr =
   | CSort of Loc.t * glob_sort
   | CCast of Loc.t * constr_expr * constr_expr cast_type
   | CNotation of Loc.t * notation * constr_notation_substitution
-  | CGeneralization of Loc.t * binding_kind * abstraction_kind option * constr_expr
+  | CGeneralization of Loc.t * implicit_status * abstraction_kind option * constr_expr
   | CPrim of Loc.t * prim_token
   | CDelimiters of Loc.t * string * constr_expr
 
@@ -132,7 +132,7 @@ and constr_notation_substitution =
     constr_expr list list * (** for recursive notations *)
     local_binder list list (** for binders subexpressions *)
 
-type typeclass_constraint = (Name.t located * Id.t located list option) * binding_kind * constr_expr
+type typeclass_constraint = (Name.t located * Id.t located list option) * implicit_status * constr_expr
 
 and typeclass_context = typeclass_constraint list
 
diff --git a/intf/decl_kinds.mli b/intf/decl_kinds.mli
index 29972f2f46..c117baf3f3 100644
--- a/intf/decl_kinds.mli
+++ b/intf/decl_kinds.mli
@@ -10,7 +10,10 @@
 
 type locality = Discharge | Local | Global
 
-type binding_kind = Explicit | Implicit
+type implicit_status = Explicit | Implicit
+
+type binding_kind = implicit_status
+(** @deprecated Alias type *)
 
 type polymorphic = bool
 
diff --git a/intf/glob_term.mli b/intf/glob_term.mli
index b3159c860c..178952fef1 100644
--- a/intf/glob_term.mli
+++ b/intf/glob_term.mli
@@ -40,8 +40,8 @@ type glob_constr =
   | GEvar of Loc.t * existential_name * (Id.t * glob_constr) list
   | GPatVar of Loc.t * (bool * patvar) (** Used for patterns only *)
   | GApp of Loc.t * glob_constr * glob_constr list
-  | GLambda of Loc.t * Name.t * binding_kind *  glob_constr * glob_constr
-  | GProd of Loc.t * Name.t * binding_kind * glob_constr * glob_constr
+  | GLambda of Loc.t * Name.t * implicit_status *  glob_constr * glob_constr
+  | GProd of Loc.t * Name.t * implicit_status * glob_constr * glob_constr
   | GLetIn of Loc.t * Name.t * glob_constr * glob_constr
   | GCases of Loc.t * case_style * glob_constr option * tomatch_tuples * cases_clauses
       (** [GCases(l,style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in [MatchStyle]) *)
@@ -54,7 +54,7 @@ type glob_constr =
   | GHole of (Loc.t * Evar_kinds.t * intro_pattern_naming_expr * Genarg.glob_generic_argument option)
   | GCast of Loc.t * glob_constr * glob_constr cast_type
 
-and glob_decl = Name.t * binding_kind * glob_constr option * glob_constr
+and glob_decl = Name.t * implicit_status * glob_constr option * glob_constr
 
 and fix_recursion_order =
   | GStructRec
-- 
cgit v1.2.3