diff --git a/library/init/meta/congruence_tactics.lean b/library/init/meta/congruence_tactics.lean
index 37399ce6cf..81fe319de9 100644
--- a/library/init/meta/congruence_tactics.lean
+++ b/library/init/meta/congruence_tactics.lean
@@ -15,6 +15,8 @@ meta constant cc_state.next         : cc_state → expr → expr
 meta constant cc_state.roots_core   : cc_state → bool → list expr
 meta constant cc_state.root         : cc_state → expr → expr
 meta constant cc_state.mt           : cc_state → expr → nat
+meta constant cc_state.gmt          : cc_state → nat
+meta constant cc_state.inc_gmt      : cc_state → cc_state
 meta constant cc_state.is_cg_root   : cc_state → expr → bool
 meta constant cc_state.pp_eqc       : cc_state → expr → tactic format
 meta constant cc_state.pp_core      : cc_state → bool → tactic format
diff --git a/src/library/tactic/congruence/congruence_closure.h b/src/library/tactic/congruence/congruence_closure.h
index 8f888a7c3d..0c1fe261eb 100644
--- a/src/library/tactic/congruence/congruence_closure.h
+++ b/src/library/tactic/congruence/congruence_closure.h
@@ -144,6 +144,7 @@ public:
         format pp_parent_occs(formatter const & fmt, expr const & e) const;
         format pp_parent_occs(formatter const & fmt) const;
         unsigned get_gmt() const { return m_gmt; }
+        void inc_gmt() { m_gmt++; }
     };
 
 private:
diff --git a/src/library/tactic/congruence/congruence_tactics.cpp b/src/library/tactic/congruence/congruence_tactics.cpp
index 17a14c6db3..6f49a80be2 100644
--- a/src/library/tactic/congruence/congruence_tactics.cpp
+++ b/src/library/tactic/congruence/congruence_tactics.cpp
@@ -109,6 +109,16 @@ vm_obj cc_state_mt(vm_obj const & ccs, vm_obj const & e) {
     return mk_vm_nat(to_cc_state(ccs).get_mt(to_expr(e)));
 }
 
+vm_obj cc_state_gmt(vm_obj const & ccs) {
+    return mk_vm_nat(to_cc_state(ccs).get_gmt());
+}
+
+vm_obj cc_state_inc_gmt(vm_obj const & ccs) {
+    congruence_closure::state s = to_cc_state(ccs);
+    s.inc_gmt();
+    return to_obj(s);
+}
+
 #define cc_state_proc(CODE)                                     \
     tactic_state const & s   = to_tactic_state(_s);             \
     try {                                                       \
@@ -333,6 +343,8 @@ void initialize_congruence_tactics() {
     DECLARE_VM_BUILTIN(name({"cc_state", "next"}),                 cc_state_next);
     DECLARE_VM_BUILTIN(name({"cc_state", "root"}),                 cc_state_root);
     DECLARE_VM_BUILTIN(name({"cc_state", "mt"}),                   cc_state_mt);
+    DECLARE_VM_BUILTIN(name({"cc_state", "gmt"}),                  cc_state_gmt);
+    DECLARE_VM_BUILTIN(name({"cc_state", "inc_gmt"}),              cc_state_inc_gmt);
     DECLARE_VM_BUILTIN(name({"cc_state", "is_cg_root"}),           cc_state_is_cg_root);
     DECLARE_VM_BUILTIN(name({"cc_state", "roots_core"}),           cc_state_roots_core);
     DECLARE_VM_BUILTIN(name({"cc_state", "internalize"}),          cc_state_internalize);