diff --git a/src/ecSection.ml b/src/ecSection.ml
index 600a4507a..4de412bcb 100644
--- a/src/ecSection.ml
+++ b/src/ecSection.ml
@@ -1249,7 +1249,7 @@ let check_tyd scenv prefix name tyd =
     check_section scenv from;
     check_polymorph scenv from tyd.tyd_params;
     check_abstract scenv from (is_abstract_ty tyd.tyd_type)
-  | `Global ->
+  | `Global when scenv.sc_insec ->
     let cd = {
         d_ty    = [`Declare; `Global];
         d_op    = [`Global];
@@ -1260,6 +1260,7 @@ let check_tyd scenv prefix name tyd =
         d_tc    = [`Global];
       } in
     on_tydecl (mkaenv scenv.sc_env (cb scenv from cd)) tyd
+  | `Global -> ()
 
 let is_abstract_op op =
   match op.op_kind with
@@ -1288,6 +1289,7 @@ let check_op scenv prefix name op =
     on_opdecl (mkaenv scenv.sc_env (cb scenv from cd)) op
 
   | `Global ->
+    if scenv.sc_insec then
     let cd = {
         d_ty    = [`Declare; `Global];
         d_op    = [`Declare; `Global];
diff --git a/src/ecUnify.ml b/src/ecUnify.ml
index 55a9a0f67..c89a697a0 100644
--- a/src/ecUnify.ml
+++ b/src/ecUnify.ml
@@ -284,8 +284,17 @@ module UniEnv = struct
     List.map (fun tv -> subst (tvar tv)) params
 
   let openty_r (ue : unienv) (params : ty_params) (tvi : tvar_inst option) =
-    let subst = f_subst_init ~tv:(opentvi ue params tvi) () in
-      (subst, subst_tv (ty_subst subst) params)
+    match params, tvi with
+    | [], None ->
+        (* No type parameter to open: the substitution is the identity
+           and there is no instance to report. Worth special-casing,
+           [openty_r] is called once per overloading candidate. A
+           non-[None] [tvi] is left to the general path, which reports
+           an arity mismatch instead of silently ignoring it. *)
+        (Fsubst.f_subst_id, [])
+    | _ ->
+      let subst = f_subst_init ~tv:(opentvi ue params tvi) () in
+        (subst, subst_tv (ty_subst subst) params)
 
   let opentys (ue : unienv) (params : ty_params) (tvi : tvar_inst option) (tys : ty list) =
     let (subst, tvs) = openty_r ue params tvi in
@@ -470,14 +479,22 @@ let select_op_outcomes
     (path, instance, op.D.op_ty, f)
   in
 
+  (* The expected type does not depend on the candidate, so build it
+     once in a scratch environment that every candidate is then forked
+     from. Building it per candidate allocated one throw-away
+     unification variable (and one arrow type) per candidate, which is
+     pure waste on the overloaded symbols: on a Jasmin extraction the
+     unary minus of an integer literal has nine candidates, eight of
+     which are discarded. *)
+  let ue0 = UniEnv.copy ue in
+  let texpected = tfun_expected ue0 ?retty psig in
+
   let select (path, op) =
-    let subue = UniEnv.copy ue in
+    let subue = UniEnv.copy ue0 in
 
     let (tip, tvs) = UniEnv.openty_r subue op.D.op_tparams tvi in
     let top = ty_subst tip op.D.op_ty in
 
-    let texpected = tfun_expected subue ?retty psig in
-
     match unify env subue top texpected with
     | () -> mk_ok (path, op) tip tvs top subue
     | exception UnificationFailure _ -> KO (lazy (classify (path, op)))