diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index 72fcff3f13..8885e32768 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -1595,7 +1595,8 @@ protected meta def apply_inj_lemma : tactic unit :=
 do h ← intro `h,
    some (lhs, rhs) ← expr.is_eq <$> infer_type h,
    (expr.const C _) ← return lhs.get_app_fn,
-   applyc (name.mk_string "inj" C),
+   -- We disable auto_param and opt_param support to address issue #1943
+   applyc (name.mk_string "inj" C) {auto_param := ff, opt_param := ff},
    assumption
 
 /- Auxiliary tactic for proving `I.C.inj_eq` lemmas.
diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index aa2dd6b7b7..1a3b6f8b2b 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -1001,8 +1001,8 @@ do env  ← get_env,
    return (expr.const c ls)
 
 /-- Apply the constant `c` -/
-meta def applyc (c : name) : tactic unit :=
-do c ← mk_const c, apply c, skip
+meta def applyc (c : name) (cfg : apply_cfg := {}) : tactic unit :=
+do c ← mk_const c, apply c cfg, skip
 
 meta def eapplyc (c : name) : tactic unit :=
 do c ← mk_const c, eapply c, skip
diff --git a/tests/lean/run/1943.lean b/tests/lean/run/1943.lean
new file mode 100644
index 0000000000..7ad8c3dcb3
--- /dev/null
+++ b/tests/lean/run/1943.lean
@@ -0,0 +1,6 @@
+open tactic
+meta def c := abstract `[assumption]
+
+structure B (U : Type) :=
+  (f : U → U)
+  (w : ∀ u : U, f u = u . c)