From 3617440d303ce674305434b9e5b930ed66ffff6d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 22 Jan 2017 13:03:39 -0800 Subject: [PATCH] chore(tests/lean/interactive/info_goal): fix expected output --- tests/lean/interactive/info_goal.lean.expected.out | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/lean/interactive/info_goal.lean.expected.out b/tests/lean/interactive/info_goal.lean.expected.out index b337ebdfe9..53f025bb4d 100644 --- a/tests/lean/interactive/info_goal.lean.expected.out +++ b/tests/lean/interactive/info_goal.lean.expected.out @@ -1,5 +1,5 @@ {"message":"file invalidated","response":"ok","seq_num":0} -{"record":{"full-id":"tactic.interactive.exact","source":{"column":9,"file":"/library/init/meta/interactive.lean","line":138},"state":"⊢ ℕ → ℕ","type":"interactive.types.qexpr0 → tactic unit"},"response":"ok","seq_num":4} +{"record":{"doc":"This tactic applies to any goal. It gives directly the exact proof\nterm of the goal. Let `T` be our goal, let `p` be a term of type `U` then\n`exact p` succeeds iff `T` and `U` are definitionally equal.","full-id":"tactic.interactive.exact","source":{"column":9,"file":"/library/init/meta/interactive.lean","line":195},"state":"⊢ ℕ → ℕ","type":"interactive.types.qexpr0 → tactic unit"},"response":"ok","seq_num":4} {"record":{"state":"no goals"},"response":"ok","seq_num":6} {"record":{"state":"no goals"},"response":"ok","seq_num":8} {"record":{"state":"⊢ ℕ → ℕ"},"response":"ok","seq_num":11}