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