From 61930c3d85f59fde5d39eae847e83ae802014ed0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 21 Feb 2018 10:28:27 -0800 Subject: [PATCH] fix(library/init/meta/comp_value_tactics): instantiate metavars --- library/init/meta/comp_value_tactics.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/init/meta/comp_value_tactics.lean b/library/init/meta/comp_value_tactics.lean index 34259f1432..ea6ed50ea5 100644 --- a/library/init/meta/comp_value_tactics.lean +++ b/library/init/meta/comp_value_tactics.lean @@ -17,7 +17,7 @@ meta constant mk_int_val_ne_proof : expr → expr → option expr namespace tactic open expr meta def comp_val : tactic unit := -do t ← target, +do t ← target >>= instantiate_mvars, guard (is_app t), type ← infer_type t.app_arg, (do is_def_eq type (const `nat []),