binder_kind Generalized: remove 1st arg as it's always Implicit

https://coq.inria.fr/distrib/current/refman/language/gallina-extensions.html#implicit-generalization
>The generalizing binders `{ } and `( ) work similarly to their
>explicit counterparts, only binding the generalized variables
>implicitly, as maximally-inserted arguments.

I guess this was meant to provide a way to get "(A:_) {B:bla A}" from
"`{B:bla A}" (where A is generalizable) but there's no syntax for it
so let's drop the ml side until such a syntax exists.

6 files changed, 14 insertions, 16 deletions

diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index 9f778d99e9..3ebbbdfb88 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -40,8 +40,8 @@ type explicitation =
 
 type binder_kind =
   | Default of binding_kind
-  | Generalized of binding_kind * binding_kind * bool
-      (** Inner binding, outer bindings, typeclass-specific flag
+  | Generalized of binding_kind * bool
+      (** (Inner binding always Implicit) Outer bindings, typeclass-specific flag
 	 for implicit generalization of superclasses *)
 
 type abstraction_kind = AbsLambda | AbsPi
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 443473d5b6..bcb2f34377 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -34,8 +34,8 @@ let abstraction_kind_eq ak1 ak2 = match ak1, ak2 with
 
 let binder_kind_eq b1 b2 = match b1, b2 with
 | Default bk1, Default bk2 -> binding_kind_eq bk1 bk2
-| Generalized (bk1, ck1, b1), Generalized (bk2, ck2, b2) ->
-  binding_kind_eq bk1 bk2 && binding_kind_eq ck1 ck2 &&
+| Generalized (ck1, b1), Generalized (ck2, b2) ->
+  binding_kind_eq ck1 ck2 &&
   (if b1 then b2 else not b2)
 | _ -> false
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f06493b374..753065b7dd 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -389,7 +389,7 @@ let push_name_env ?(global_level=false) ntnvars implargs env =
       {env with ids = Id.Set.add id env.ids; impls = Id.Map.add id implargs env.impls}
 
 let intern_generalized_binder ?(global_level=false) intern_type ntnvars
-    env {loc;v=na} b b' t ty =
+    env {loc;v=na} b' t ty =
   let ids = (match na with Anonymous -> fun x -> x | Name na -> Id.Set.add na) env.ids in
   let ty, ids' =
     if t then ty, ids else
@@ -403,7 +403,7 @@ let intern_generalized_binder ?(global_level=false) intern_type ntnvars
     env fvs in
   let bl = List.map
     CAst.(map (fun id ->
-      (Name id, b, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None))))
+      (Name id, Implicit, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None))))
     fvs
   in
   let na = match na with
@@ -433,8 +433,8 @@ let intern_assumption intern ntnvars env nal bk ty =
           (push_name_env ntnvars impls env locna,
            (make ?loc (na,k,locate_if_hole ?loc na ty))::bl))
 	(env, []) nal
-  | Generalized (b,b',t) ->
-     let env, b = intern_generalized_binder intern_type ntnvars env (List.hd nal) b b' t ty in
+  | Generalized (b',t) ->
+     let env, b = intern_generalized_binder intern_type ntnvars env (List.hd nal) b' t ty in
      env, b
 
 let glob_local_binder_of_extended = DAst.with_loc_val (fun ?loc -> function
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 8d45290ac0..f71ad14dd4 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -196,10 +196,9 @@ let combine_params avoid fn applied needed =
 	  user_err ?loc:(Constrexpr_ops.constr_loc x) (str "Typeclass does not expect more arguments")
   in aux [] avoid applied needed
 
-let combine_params_freevar =
-  fun avoid (_, decl) ->
-    let id' = next_name_away_from (RelDecl.get_name decl) avoid in
-      (CAst.make @@ CRef (qualid_of_ident id',None), Id.Set.add id' avoid)
+let combine_params_freevar avoid (_, decl) =
+  let id' = next_name_away_from (RelDecl.get_name decl) avoid in
+  (CAst.make @@ CRef (qualid_of_ident id',None), Id.Set.add id' avoid)
 
 let destClassApp cl =
   let open CAst in
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index 4a9190c10a..6df97609f5 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -500,9 +500,9 @@ GRAMMAR EXTEND Gram
       | "{"; id=name; idl=LIST1 name; "}" ->
           { List.map (fun id -> CLocalAssum ([id],Default Implicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) (id::idl) }
       | "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" ->
-	  { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, Explicit, b), t)) tc }
+          { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Explicit, b), t)) tc }
       | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" ->
-	  { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, Implicit, b), t)) tc }
+          { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, b), t)) tc }
       | "'"; p = pattern LEVEL "0" ->
           { let (p, ty) =
             match p.CAst.v with
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 78733784a7..9d3ed40f6c 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -339,8 +339,7 @@ let tag_var = tag Tag.variable
 
   let pr_binder many pr (nal,k,t) =
     match k with
-      | Generalized (b, b', t') ->
-        assert (match b with Implicit -> true | _ -> false);
+      | Generalized (b', t') ->
         begin match nal with
           |[{loc; v=Anonymous}] ->
             hov 1 (str"`" ++ (surround_impl b'