From 8e9997e2530696a307fbe9ba35964dc149842df6 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 21 Apr 2015 19:52:01 -0700
Subject: [PATCH] chore(tests/lean/interactive/sec_info_bug): remove 'context'
 command from test

---
 tests/lean/interactive/sec_info_bug.input | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/lean/interactive/sec_info_bug.input b/tests/lean/interactive/sec_info_bug.input
index c56e417de4..e32704304f 100644
--- a/tests/lean/interactive/sec_info_bug.input
+++ b/tests/lean/interactive/sec_info_bug.input
@@ -3,7 +3,7 @@ SYNC 10
 import logic
 constant category : Type -> Type
 namespace category
-  context
+  section
   parameters {ob : Type} {C : category ob}
   variables {a b c d : ob}
   definition hom : ob → ob → Type := let aux := C in sorry