Merge remote-tracking branch 'github/pr/283' into trunk

Was PR#283: Stylistic improvements in intf/decl_kinds.mli.

3 files changed, 18 insertions, 11 deletions

diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index 0cbb29575..e494b2f81 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 6a4e18833..c117baf3f 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
 
@@ -49,9 +52,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 assumption_kind = assumption_object_kind declaration_kind
 
-type definition_kind = locality * polymorphic * definition_object_kind
+type definition_kind = definition_object_kind declaration_kind
 
 (** Kinds used in proofs *)
 
@@ -59,7 +66,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 *)
 
diff --git a/intf/glob_term.mli b/intf/glob_term.mli
index b3159c860..178952fef 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