From 4197f42c15f0116eeb58df5b64b60f2fa6f6951f Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 16 May 2019 13:59:25 +0200
Subject: Cleanup Implicit_quantifiers.implicit_application

- fix misleading indentation
- simplify "let a, b = e in a, b" -> "e"
---
 interp/implicit_quantifiers.ml | 48 ++++++++++++++++++++----------------------
 1 file changed, 23 insertions(+), 25 deletions(-)

(limited to 'interp/implicit_quantifiers.ml')

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index dffccf02fc..8d45290ac0 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -223,33 +223,31 @@ let implicit_application env ?(allow_partial=true) f ty =
     try
       let ({CAst.v=(qid, _, _)} as clapp) = destClassAppExpl ty in
       let gr = Nametab.locate qid in
-	if Typeclasses.is_class gr then Some (clapp, gr) else None
+      if Typeclasses.is_class gr then Some (clapp, gr) else None
     with Not_found -> None
   in
-    match is_class with
-    | None -> ty, env
-    | Some ({CAst.loc;v=(id, par, inst)}, gr) ->
-	let avoid = Id.Set.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in
-	let c, avoid =
-   let env = Global.env () in
-   let sigma = Evd.from_env env in
-   let c = class_info env sigma gr in
-   let (ci, rd) = c.cl_context in
-   if not allow_partial then
-     begin
-       let opt_succ x n = match x with
-         | None -> succ n
-         | Some _ -> n
-       in
-       let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in
-       let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in
-       if not (Int.equal needlen applen) then
-         mismatched_ctx_inst_err (Global.env ()) Typeclasses_errors.Parameters (List.map fst par) rd
-     end;
-   let pars = List.rev (List.combine ci rd) in
-   let args, avoid = combine_params avoid f par pars in
-   CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid
- in c, avoid
+  match is_class with
+  | None -> ty, env
+  | Some ({CAst.loc;v=(id, par, inst)}, gr) ->
+    let avoid = Id.Set.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in
+    let env = Global.env () in
+    let sigma = Evd.from_env env in
+    let c = class_info env sigma gr in
+    let (ci, rd) = c.cl_context in
+    if not allow_partial then
+      begin
+        let opt_succ x n = match x with
+          | None -> succ n
+          | Some _ -> n
+        in
+        let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in
+        let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in
+        if not (Int.equal needlen applen) then
+          mismatched_ctx_inst_err (Global.env ()) Typeclasses_errors.Parameters (List.map fst par) rd
+      end;
+    let pars = List.rev (List.combine ci rd) in
+    let args, avoid = combine_params avoid f par pars in
+    CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid
 
 let warn_ignoring_implicit_status =
   CWarnings.create ~name:"ignoring_implicit_status" ~category:"implicits"
-- 
cgit v1.2.3


From 21269d0fef6794a672c36abdc5760889adc0e09c Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 16 May 2019 14:21:37 +0200
Subject: 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.
---
 interp/implicit_quantifiers.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'interp/implicit_quantifiers.ml')

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
-- 
cgit v1.2.3


From 11533785773269d9632ef8925ed34ea2d541818b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 16 May 2019 14:32:09 +0200
Subject: Fix #10176: shadowing vs automatic class based generalization

---
 interp/implicit_quantifiers.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'interp/implicit_quantifiers.ml')

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index f71ad14dd4..851109876b 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -221,8 +221,10 @@ let implicit_application env ?(allow_partial=true) f ty =
   let is_class =
     try
       let ({CAst.v=(qid, _, _)} as clapp) = destClassAppExpl ty in
-      let gr = Nametab.locate qid in
-      if Typeclasses.is_class gr then Some (clapp, gr) else None
+      if Libnames.idset_mem_qualid qid env then None
+      else
+        let gr = Nametab.locate qid in
+        if Typeclasses.is_class gr then Some (clapp, gr) else None
     with Not_found -> None
   in
   match is_class with
-- 
cgit v1.2.3