Functionalize env in type classes

I had to reorganize the code a bit. The Context command moved to
comAssumption, as it is not so related to type classes. We were able to
remove a few hooks on the way.

1 files changed, 19 insertions, 17 deletions

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 854651e7b7..dffccf02fc 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -231,23 +231,25 @@ let implicit_application env ?(allow_partial=true) f ty =
     | 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 c = class_info 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
+   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
 
 let warn_ignoring_implicit_status =
   CWarnings.create ~name:"ignoring_implicit_status" ~category:"implicits"