From eda1efcb5f2448bc0d072aab4b37cf9caa14720c Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Tue, 29 Aug 2017 16:34:59 +0200
Subject: [PATCH] fix(library/init/meta/congr_tactic): export congr as an
 interactive tactic

---
 library/init/meta/congr_tactic.lean | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/library/init/meta/congr_tactic.lean b/library/init/meta/congr_tactic.lean
index 96b6e7e82f..4a3dd5c8bb 100644
--- a/library/init/meta/congr_tactic.lean
+++ b/library/init/meta/congr_tactic.lean
@@ -56,4 +56,11 @@ do focus1 (try assumption >> congr_core >> all_goals (try reflexivity >> try con
 meta def rel_congr : tactic unit :=
 do focus1 (try assumption >> rel_congr_core >> all_goals (try reflexivity))
 
+namespace interactive
+
+meta def congr := tactic.congr
+meta def rel_congr := tactic.rel_congr
+
+end interactive
+
 end tactic