From c3756b49eb398cbbc2dcc159a7a3b74f8fe5abcc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 10 Nov 2019 09:04:23 -0800
Subject: [PATCH] chore: fix tests

---
 tests/lean/mvar1.lean | 12 ++++++------
 tests/lean/mvar2.lean |  6 +++---
 tests/lean/mvar3.lean |  8 ++++----
 3 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/tests/lean/mvar1.lean b/tests/lean/mvar1.lean
index 9af083b0cd..dca48246e0 100644
--- a/tests/lean/mvar1.lean
+++ b/tests/lean/mvar1.lean
@@ -49,12 +49,12 @@ def t1 := lctx5.mkLambda #[α, x, y] $ mkApp f #[α, mkApp g #[x, y], lctx5.mkLa
 #eval t1
 
 def mctx1 : MetavarContext := {}
-def mctx2  := mctx1.mkDecl `m1 `m1 lctx3 natE
-def mctx3  := mctx2.mkDecl `m2 `m2 lctx4 α
-def mctx4  := mctx3.mkDecl `m3 `m3 lctx4 natE
-def mctx5  := mctx4.mkDecl `m4 `m4 lctx1 (arrow typeE (arrow natE (arrow α natE)))
-def mctx6  := mctx5.mkDecl `m5 `m5 lctx5 typeE
-def mctx7  := mctx5.mkDecl `m6 `m6 lctx5 (arrow typeE (arrow natE (arrow α natE)))
+def mctx2  := mctx1.addExprMVarDecl `m1 `m1 lctx3 natE
+def mctx3  := mctx2.addExprMVarDecl `m2 `m2 lctx4 α
+def mctx4  := mctx3.addExprMVarDecl `m3 `m3 lctx4 natE
+def mctx5  := mctx4.addExprMVarDecl `m4 `m4 lctx1 (arrow typeE (arrow natE (arrow α natE)))
+def mctx6  := mctx5.addExprMVarDecl `m5 `m5 lctx5 typeE
+def mctx7  := mctx5.addExprMVarDecl `m6 `m6 lctx5 (arrow typeE (arrow natE (arrow α natE)))
 def mctx8  := mctx7.assignDelayed `m4 lctx4 #[α, x, y] m3
 def mctx9  := mctx8.assignExpr `m3 (mkApp g #[x, y])
 def mctx10 := mctx9.assignExpr `m1 a
diff --git a/tests/lean/mvar2.lean b/tests/lean/mvar2.lean
index 0b0881d1e2..beb283407f 100644
--- a/tests/lean/mvar2.lean
+++ b/tests/lean/mvar2.lean
@@ -40,9 +40,9 @@ def lctx3 := lctx2.mkLocalDecl `x `x m1
 def lctx4 := lctx3.mkLocalDecl `y `y (arrow natE (mkApp m3 #[α, x]))
 
 def mctx1 : MetavarContext := {}
-def mctx2  := mctx1.mkDecl `m1 `m1 lctx1 typeE
-def mctx3  := mctx2.mkDecl `m2 `m2 lctx3 natE
-def mctx4  := mctx3.mkDecl `m3 `m3 lctx1 (arrow typeE (arrow natE natE))
+def mctx2  := mctx1.addExprMVarDecl `m1 `m1 lctx1 typeE
+def mctx3  := mctx2.addExprMVarDecl `m2 `m2 lctx3 natE
+def mctx4  := mctx3.addExprMVarDecl `m3 `m3 lctx1 (arrow typeE (arrow natE natE))
 def mctx5  := mctx4.assignDelayed `m3 lctx3 #[α, x] m2
 def mctx6  := mctx5.assignExpr `m2 (arrow α α)
 def mctx7  := mctx6.assignExpr `m1 natE
diff --git a/tests/lean/mvar3.lean b/tests/lean/mvar3.lean
index 0bacf3fe15..f5e94f53ab 100644
--- a/tests/lean/mvar3.lean
+++ b/tests/lean/mvar3.lean
@@ -46,10 +46,10 @@ def lctx3 := lctx2.mkLocalDecl `x `x m1
 def lctx4 := lctx3.mkLocalDecl `y `y (arrow natE m2)
 
 def mctx1 : MetavarContext := {}
-def mctx2  := mctx1.mkDecl `m1 `m1 lctx2 typeE
-def mctx3  := mctx2.mkDecl `m2 `m2 lctx3 natE
-def mctx4  := mctx3.mkDecl `m3 `m3 lctx3 natE
-def mctx4' := mctx3.mkDecl `m3 `m3 lctx3 natE true
+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 R1 :=
 match mkLambda mctx4 {namePrefix := `n} lctx4 #[α, x, y] $ mkApp f #[m3, x] with