From 1e2157e210e7a6edc4cd5772447a431a0b71d653 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Mon, 19 Jun 2017 03:56:14 -0400 Subject: [PATCH] fix(init/meta/constructor_tactic): constructor tac uses whnf --- library/init/meta/constructor_tactic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/init/meta/constructor_tactic.lean b/library/init/meta/constructor_tactic.lean index 58f7f075b5..51327623ea 100644 --- a/library/init/meta/constructor_tactic.lean +++ b/library/init/meta/constructor_tactic.lean @@ -19,7 +19,7 @@ private meta def try_constructors (cfg : apply_cfg): list name → tactic unit | (c::cs) := (mk_const c >>= λ e, apply_core e cfg >> return ()) <|> try_constructors cs meta def constructor (cfg : apply_cfg := {}): tactic unit := -target >>= instantiate_mvars >>= get_constructors_for >>= try_constructors cfg +target >>= instantiate_mvars >>= whnf >>= get_constructors_for >>= try_constructors cfg meta def econstructor : tactic unit := constructor {new_goals := new_goals.non_dep_only}