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

I hadn't realized that this PR uses OCaml's 4.03 inlined records
feature. I will advocate again for a switch to the latest OCaml stable
version, but meanwhile, let's revert. Sorry for the noise.

This reverts commit 3c47248abc27aa9c64120db30dcb0d7bf945bc70, reversing
changes made to ceb68d1d643ac65f500e0201f61e73cf22e6e2fb.

3 files changed, 11 insertions, 18 deletions

diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index e494b2f81..0cbb29575 100644
--- a/intf/constrexpr.mli
+++ b/intf/constrexpr.mli
@@ -23,8 +23,8 @@ type explicitation =
   | ExplByName of Id.t
 
 type binder_kind =
-  | Default of implicit_status
-  | Generalized of implicit_status * implicit_status * bool
+  | Default of binding_kind
+  | Generalized of binding_kind * binding_kind * 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 * implicit_status * abstraction_kind option * constr_expr
+  | CGeneralization of Loc.t * binding_kind * 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) * implicit_status * constr_expr
+type typeclass_constraint = (Name.t located * Id.t located list option) * binding_kind * constr_expr
 
 and typeclass_context = typeclass_constraint list
 
diff --git a/intf/decl_kinds.mli b/intf/decl_kinds.mli
index c117baf3f..6a4e18833 100644
--- a/intf/decl_kinds.mli
+++ b/intf/decl_kinds.mli
@@ -10,10 +10,7 @@
 
 type locality = Discharge | Local | Global
 
-type implicit_status = Explicit | Implicit
-
-type binding_kind = implicit_status
-(** @deprecated Alias type *)
+type binding_kind = Explicit | Implicit
 
 type polymorphic = bool
 
@@ -52,13 +49,9 @@ type assumption_object_kind = Definitional | Logical | Conjectural
    Logical      |  Hypothesis | Axiom
 
 *)
-type 'a declaration_kind = { locality : locality;
-                             polymorphic : bool;
-                             object_kind : 'a }
-
-type assumption_kind = assumption_object_kind declaration_kind
+type assumption_kind = locality * polymorphic * assumption_object_kind
 
-type definition_kind = definition_object_kind declaration_kind
+type definition_kind = locality * polymorphic * definition_object_kind
 
 (** Kinds used in proofs *)
 
@@ -66,7 +59,7 @@ type goal_object_kind =
   | DefinitionBody of definition_object_kind
   | Proof of theorem_kind
 
-type goal_kind = goal_object_kind declaration_kind
+type goal_kind = locality * polymorphic * goal_object_kind
 
 (** Kinds used in library *)
 
diff --git a/intf/glob_term.mli b/intf/glob_term.mli
index 178952fef..b3159c860 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 * implicit_status *  glob_constr * glob_constr
-  | GProd of Loc.t * Name.t * implicit_status * glob_constr * glob_constr
+  | GLambda of Loc.t * Name.t * binding_kind *  glob_constr * glob_constr
+  | GProd of Loc.t * Name.t * binding_kind * 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 * implicit_status * glob_constr option * glob_constr
+and glob_decl = Name.t * binding_kind * glob_constr option * glob_constr
 
 and fix_recursion_order =
   | GStructRec