From 65edd6e37cbab9ff7deb89631ec96b771a5d95ee Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 17 Dec 2019 07:37:58 -0800
Subject: [PATCH] chore: fix tests

---
 tests/lean/mvar3.lean      | 2 +-
 tests/lean/run/tactic.lean | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/lean/mvar3.lean b/tests/lean/mvar3.lean
index e7e1603bc8..18fe18d0f8 100644
--- a/tests/lean/mvar3.lean
+++ b/tests/lean/mvar3.lean
@@ -49,7 +49,7 @@ def mctx1 : MetavarContext := {}
 def mctx2  := mctx1.addExprMVarDecl `m1 `m1 lctx2 #[] typeE
 def mctx3  := mctx2.addExprMVarDecl `m2 `m2 lctx3 #[] natE
 def mctx4  := mctx3.addExprMVarDecl `m3 `m3 lctx3 #[] natE
-def mctx4' := mctx3.addExprMVarDecl `m3 `m3 lctx3 #[] natE true
+def mctx4' := mctx3.addExprMVarDecl `m3 `m3 lctx3 #[] natE MetavarKind.syntheticOpaque
 
 def R1 :=
 match mkLambdaTest mctx4 {namePrefix := `n} lctx4 #[α, x, y] $ mkAppN f #[m3, x] with
diff --git a/tests/lean/run/tactic.lean b/tests/lean/run/tactic.lean
index 5f95557887..e6488b060f 100644
--- a/tests/lean/run/tactic.lean
+++ b/tests/lean/run/tactic.lean
@@ -11,7 +11,7 @@ set_option trace.Meta.Tactic true
 
 def tst1 : MetaM Unit :=
 do cinfo ← getConstInfo `simple;
-   mvar  ← mkFreshExprSyntheticMVar cinfo.type;
+   mvar  ← mkFreshExprSyntheticOpaqueMVar cinfo.type;
    let mvarId := mvar.mvarId!;
    (_, mvarId) ← introN mvarId 4;
    assumption mvarId;