From 52894e97f045c257ba5f4a7c9d64c48fa1913994 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 12 Aug 2020 14:14:37 +0200
Subject: Cosmetic changes as suggested by SkySkimmer.

---
 tactics/class_tactics.ml | 7 ++-----
 tactics/hints.ml         | 5 ++---
 2 files changed, 4 insertions(+), 8 deletions(-)

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 1fadc164bf..36544883aa 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -179,11 +179,8 @@ let unify_resolve_refine flags h diff =
     let ty = Retyping.get_type_of env sigma term in
     let sigma, cl = Clenv.make_evar_clause env sigma ?len ty in
     let term = applist (term, List.map (fun x -> x.hole_evar) cl.cl_holes) in
-    let sigma =
-      Evarconv.(unify_leq_delay
-                  ~flags:(default_flags_of flags.core_unify_flags.modulo_delta)
-                            env sigma cl.cl_concl concl)
-    in
+    let flags = Evarconv.default_flags_of flags.core_unify_flags.modulo_delta in
+    let sigma = Evarconv.unify_leq_delay ~flags env sigma cl.cl_concl concl in
     (sigma, term)
     end
   end
diff --git a/tactics/hints.ml b/tactics/hints.ml
index e029e4628d..7b203c3d51 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1608,13 +1608,12 @@ let connect_hint_clenv h gl =
     let emap c = Vars.subst_univs_level_constr subst c in
     let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
     (* Only metas are mentioning the old universes. *)
-    let clenv = {
+    {
       templval = Evd.map_fl emap clenv.templval;
       templtyp = Evd.map_fl emap clenv.templtyp;
       evd = Evd.map_metas emap evd;
       env = Proofview.Goal.env gl;
-    } in
-    clenv
+    }
   else
     let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
     { clenv with evd = evd ; env = Proofview.Goal.env gl }
-- 
cgit v1.2.3