From 5c79973300a88d72ea7cce483fb60f8451945c09 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott@tqft.net>
Date: Tue, 19 Jul 2022 14:02:31 +1000
Subject: [PATCH] feat: allow an `ApplyConfig` argument at `constructor` tactic
 (#1319)

---
 src/Lean/Meta/Tactic/Constructor.lean | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Constructor.lean b/src/Lean/Meta/Tactic/Constructor.lean
index 29b6132866..93ab123660 100644
--- a/src/Lean/Meta/Tactic/Constructor.lean
+++ b/src/Lean/Meta/Tactic/Constructor.lean
@@ -9,7 +9,11 @@ import Lean.Meta.Tactic.Apply
 
 namespace Lean.Meta
 
-def constructor (mvarId : MVarId) : MetaM (List MVarId) := do
+/--
+When the goal `mvarId` is an inductive datatype,
+`constructor` calls `apply` with the first matching constructor.
+-/
+def constructor (mvarId : MVarId) (cfg : ApplyConfig := {}) : MetaM (List MVarId) := do
   withMVarContext mvarId do
     checkNotAssigned mvarId `constructor
     let target ← getMVarType' mvarId
@@ -18,7 +22,7 @@ def constructor (mvarId : MVarId) : MetaM (List MVarId) := do
       fun ival us => do
         for ctor in ival.ctors do
           try
-            return ← apply mvarId (Lean.mkConst ctor us)
+            return ← apply mvarId (Lean.mkConst ctor us) cfg
           catch _ =>
             pure ()
         throwTacticEx `constructor mvarId "no applicable constructor found"