From 5113f6b9d84000c8e4fd72ec99e3e001c4d741ec Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 7 May 2015 10:01:28 -0700 Subject: [PATCH] fix(tests/lean): test output to reflect recent changes --- tests/lean/revert_fail.lean.expected.out | 6 +++++- tests/lean/rewrite_fail.lean.expected.out | 6 +++++- 2 files changed, 10 insertions(+), 2 deletions(-) diff --git a/tests/lean/revert_fail.lean.expected.out b/tests/lean/revert_fail.lean.expected.out index a27c50060..6ac2c7c0d 100644 --- a/tests/lean/revert_fail.lean.expected.out +++ b/tests/lean/revert_fail.lean.expected.out @@ -13,8 +13,12 @@ revert_fail.lean:6:0: error: failed to add declaration '14.0' to environment, va remark: set 'formatter.hide_full_terms' to false to see the complete term λ (A : Type) (n : nat) (v : …), ?M_1 -revert_fail.lean:11:2: error: tactic failed +revert_fail.lean:11:2: error:invalid tactic, there are no goals to be solved +proof state: no goals +revert_fail.lean:12:0: error: don't know how to synthesize placeholder +n : nat +⊢ n = n revert_fail.lean:12:0: error: failed to add declaration '14.1' to environment, value has metavariables remark: set 'formatter.hide_full_terms' to false to see the complete term λ (n : nat), diff --git a/tests/lean/rewrite_fail.lean.expected.out b/tests/lean/rewrite_fail.lean.expected.out index 0ffde0242..2ecd71ab4 100644 --- a/tests/lean/rewrite_fail.lean.expected.out +++ b/tests/lean/rewrite_fail.lean.expected.out @@ -15,8 +15,12 @@ rewrite_fail.lean:6:0: error: failed to add declaration '14.0' to environment, v remark: set 'formatter.hide_full_terms' to false to see the complete term λ (a b : ℕ) (Ha : …) (Hb : …), ?M_1 -rewrite_fail.lean:11:2: error: tactic failed +rewrite_fail.lean:11:2: error:invalid tactic, there are no goals to be solved +proof state: no goals +rewrite_fail.lean:12:0: error: don't know how to synthesize placeholder +a : ℕ +⊢ a = a rewrite_fail.lean:12:0: error: failed to add declaration '14.1' to environment, value has metavariables remark: set 'formatter.hide_full_terms' to false to see the complete term λ (a : ℕ),