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.

7 files changed, 18 insertions, 18 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 2644a56b3d..59c24900d2 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -17,7 +17,7 @@ open Decl_kinds
 (***********************)
 (* For binders parsing *)
 
-let implicit_status_eq bk1 bk2 = match bk1, bk2 with
+let binding_kind_eq bk1 bk2 = match bk1, bk2 with
 | Explicit, Explicit -> true
 | Implicit, Implicit -> true
 | _ -> false
@@ -28,9 +28,9 @@ let abstraction_kind_eq ak1 ak2 = match ak1, ak2 with
 | _ -> false
 
 let binder_kind_eq b1 b2 = match b1, b2 with
-| Default bk1, Default bk2 -> implicit_status_eq bk1 bk2
+| Default bk1, Default bk2 -> binding_kind_eq bk1 bk2
 | Generalized (bk1, ck1, b1), Generalized (bk2, ck2, b2) ->
-  implicit_status_eq bk1 bk2 && implicit_status_eq ck1 ck2 &&
+  binding_kind_eq bk1 bk2 && binding_kind_eq ck1 ck2 &&
   (if b1 then b2 else not b2)
 | _ -> false
 
@@ -165,7 +165,7 @@ let rec constr_expr_eq e1 e2 =
   | CPrim(_,i1), CPrim(_,i2) ->
     prim_token_eq i1 i2
   | CGeneralization (_, bk1, ak1, e1), CGeneralization (_, bk2, ak2, e2) ->
-    implicit_status_eq bk1 bk2 &&
+    binding_kind_eq bk1 bk2 &&
     Option.equal abstraction_kind_eq ak1 ak2 &&
     constr_expr_eq e1 e2
   | CDelimiters(_,s1,e1), CDelimiters(_,s2,e2) ->
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index bfe546ba5c..a92da035f6 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -26,8 +26,8 @@ val constr_expr_eq : constr_expr -> constr_expr -> bool
 val local_binder_eq : local_binder -> local_binder -> bool
 (** Equality on [local_binder]. Same properties as [constr_expr_eq]. *)
 
-val implicit_status_eq : Decl_kinds.implicit_status -> Decl_kinds.implicit_status -> bool
-(** Equality on [implicit_status] *)
+val binding_kind_eq : Decl_kinds.binding_kind -> Decl_kinds.binding_kind -> bool
+(** Equality on [binding_kind] *)
 
 val binder_kind_eq : binder_kind -> binder_kind -> bool
 (** Equality on [binder_kind] *)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 62cb62f493..f7fcbb4eed 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -808,7 +808,7 @@ and factorize_prod scopes vars na bk aty c =
   let c = extern_typ scopes vars c in
   match na, c with
   | Name id, CProdN (loc,[nal,Default bk',ty],c)
-      when implicit_status_eq bk bk' && constr_expr_eq aty ty
+      when binding_kind_eq bk bk' && constr_expr_eq aty ty
       && not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) ->
       nal,c
   | _ ->
@@ -818,7 +818,7 @@ and factorize_lambda inctx scopes vars na bk aty c =
   let c = sub_extern inctx scopes vars c in
   match c with
   | CLambdaN (loc,[nal,Default bk',ty],c)
-      when implicit_status_eq bk bk' && constr_expr_eq aty ty
+      when binding_kind_eq bk bk' && constr_expr_eq aty ty
       && not (occur_name na ty) (* avoid na in ty escapes scope *) ->
       nal,c
   | _ ->
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 863f33b18e..0e56020783 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -65,7 +65,7 @@ type var_internalization_data =
 type internalization_env =
     (var_internalization_data) Id.Map.t
 
-type glob_binder = (Name.t * implicit_status * glob_constr option * glob_constr)
+type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr)
 
 type ltac_sign = {
   ltac_vars : Id.Set.t;
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 718aa753e5..eea76aa310 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -75,7 +75,7 @@ type ltac_sign = {
 
 val empty_ltac_sign : ltac_sign
 
-type glob_binder = (Name.t * implicit_status * glob_constr option * glob_constr)
+type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr)
 
 (** {6 Internalization performs interpretation of global names and notations } *)
 
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index c65d43db36..6b29b6d3df 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -29,10 +29,10 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with
   | GVar (_,v1), GVar (_,v2) -> on_true_do (Id.equal v1 v2) add (Name v1)
   | GApp (_,f1,l1), GApp (_,f2,l2) -> f f1 f2 && List.for_all2eq f l1 l2
   | GLambda (_,na1,bk1,ty1,c1), GLambda (_,na2,bk2,ty2,c2)
-    when Name.equal na1 na2 && Constrexpr_ops.implicit_status_eq bk1 bk2 ->
+    when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 ->
     on_true_do (f ty1 ty2 && f c1 c2) add na1
   | GProd (_,na1,bk1,ty1,c1), GProd (_,na2,bk2,ty2,c2)
-    when Name.equal na1 na2 && Constrexpr_ops.implicit_status_eq bk1 bk2 ->
+    when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 ->
       on_true_do (f ty1 ty2 && f c1 c2) add na1
   | GHole _, GHole _ -> true
   | GSort (_,s1), GSort (_,s2) -> Miscops.glob_sort_eq s1 s2
@@ -772,18 +772,18 @@ let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma)
       | GHole _, _ -> v'
       | _, GHole _ -> v
       | _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v else raise No_match in
-    let unify_implicit_status bk bk' = if bk == bk' then bk' else raise No_match in
+    let unify_binding_kind bk bk' = if bk == bk' then bk' else raise No_match in
     let unify_binder alp b b' =
       match b, b' with
       | (Inl na, bk, None, t), (Inl na', bk', None, t') (* assum *) ->
          let alp, na = unify_name alp na na' in
-         alp, (Inl na, unify_implicit_status bk bk', None, unify_term alp t t')
+         alp, (Inl na, unify_binding_kind bk bk', None, unify_term alp t t')
       | (Inl na, bk, Some c, t), (Inl na', bk', Some c', t') (* let *) ->
          let alp, na = unify_name alp na na' in
-         alp, (Inl na, unify_implicit_status bk bk', Some (unify_term alp c c'), unify_term alp t t')
+         alp, (Inl na, unify_binding_kind bk bk', Some (unify_term alp c c'), unify_term alp t t')
       | (Inr p, bk, None, t), (Inr p', bk', None, t') (* pattern *) ->
          let alp, p = unify_pat alp p p' in
-         alp, (Inr p, unify_implicit_status bk bk', None, unify_term alp t t')
+         alp, (Inr p, unify_binding_kind bk bk', None, unify_term alp t t')
       | _ -> raise No_match in
     let rec unify alp bl bl' =
     match bl, bl' with
@@ -1122,7 +1122,7 @@ let term_of_binder = function
   | Anonymous -> GHole (Loc.ghost,Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None)
 
 type glob_decl2 =
-    (name, cases_pattern) Util.union * Decl_kinds.implicit_status *
+    (name, cases_pattern) Util.union * Decl_kinds.binding_kind *
       glob_constr option * glob_constr
 
 let match_notation_constr u c (metas,pat) =
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index 6428ccab66..854e222e30 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.implicit_status *
+    (name, cases_pattern) Util.union * Decl_kinds.binding_kind *
       glob_constr option * glob_constr
 val match_notation_constr : bool -> glob_constr -> interpretation ->
       (glob_constr * subscopes) list * (glob_constr list * subscopes) list *