From 4dc27fb43b105dc58d7249516b03a793f96ab3d5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 16 Nov 2015 18:30:59 -0800
Subject: [PATCH] chore(library/blast): use "override" consistently for
 proof_step objects

---
 src/library/blast/backward_action.cpp     | 2 +-
 src/library/blast/intros_action.cpp       | 2 +-
 src/library/blast/no_confusion_action.cpp | 2 +-
 src/library/blast/recursor_action.cpp     | 2 +-
 src/library/blast/revert_action.cpp       | 2 +-
 src/library/blast/simplify_actions.cpp    | 2 +-
 src/library/blast/subst_action.cpp        | 2 +-
 7 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/library/blast/backward_action.cpp b/src/library/blast/backward_action.cpp
index 7d8328efe..cf0be64b1 100644
--- a/src/library/blast/backward_action.cpp
+++ b/src/library/blast/backward_action.cpp
@@ -24,7 +24,7 @@ struct backward_proof_step_cell : public proof_step_cell {
 
     virtual ~backward_proof_step_cell() {}
 
-    virtual action_result resolve(expr const & pr) const {
+    virtual action_result resolve(expr const & pr) const override {
         state & s = curr_state();
         s.set_branch(m_branch);
         expr mvar = head(m_mvars);
diff --git a/src/library/blast/intros_action.cpp b/src/library/blast/intros_action.cpp
index 1ef5da72a..e26b72547 100644
--- a/src/library/blast/intros_action.cpp
+++ b/src/library/blast/intros_action.cpp
@@ -15,7 +15,7 @@ namespace blast {
 struct intros_proof_step_cell : public proof_step_cell {
     list<expr> m_new_hs;
     virtual ~intros_proof_step_cell() {}
-    virtual action_result resolve(expr const & pr) const {
+    virtual action_result resolve(expr const & pr) const override {
         expr new_pr = mk_proof_lambda(curr_state(), m_new_hs, pr);
         return action_result::solved(new_pr);
     }
diff --git a/src/library/blast/no_confusion_action.cpp b/src/library/blast/no_confusion_action.cpp
index f9fa6b148..42af37577 100644
--- a/src/library/blast/no_confusion_action.cpp
+++ b/src/library/blast/no_confusion_action.cpp
@@ -18,7 +18,7 @@ struct no_confusion_proof_step_cell : public proof_step_cell {
         m_I_name(I_name), m_target(t), m_eq_href(e), m_num_new_eqs(n) {}
     virtual ~no_confusion_proof_step_cell() {}
 
-    virtual action_result resolve(expr const & pr) const {
+    virtual action_result resolve(expr const & pr) const override {
         try {
             expr it   = pr;
             bool skip = true;
diff --git a/src/library/blast/recursor_action.cpp b/src/library/blast/recursor_action.cpp
index ee2e3ef5d..d15d58856 100644
--- a/src/library/blast/recursor_action.cpp
+++ b/src/library/blast/recursor_action.cpp
@@ -63,7 +63,7 @@ struct recursor_proof_step_cell : public proof_step_cell {
 
     virtual ~recursor_proof_step_cell() {}
 
-    virtual action_result resolve(expr const & pr) const {
+    virtual action_result resolve(expr const & pr) const override {
         state & s = curr_state();
         s.set_branch(m_branch);
         if (!m_dep) {
diff --git a/src/library/blast/revert_action.cpp b/src/library/blast/revert_action.cpp
index b26240ec6..4988cab9a 100644
--- a/src/library/blast/revert_action.cpp
+++ b/src/library/blast/revert_action.cpp
@@ -15,7 +15,7 @@ struct revert_proof_step_cell : public proof_step_cell {
 
     virtual ~revert_proof_step_cell() {}
 
-    virtual action_result resolve(expr const & pr) const {
+    virtual action_result resolve(expr const & pr) const override {
         expr new_pr = mk_app(pr, m_hs);
         return action_result::solved(new_pr);
     }
diff --git a/src/library/blast/simplify_actions.cpp b/src/library/blast/simplify_actions.cpp
index dcc72de39..b881c04e2 100644
--- a/src/library/blast/simplify_actions.cpp
+++ b/src/library/blast/simplify_actions.cpp
@@ -24,7 +24,7 @@ public:
 
     virtual ~simplify_target_proof_step_cell() {}
 
-    virtual action_result resolve(expr const & pr) const {
+    virtual action_result resolve(expr const & pr) const override {
         try {
             app_builder & b = get_app_builder();
             if (m_iff)
diff --git a/src/library/blast/subst_action.cpp b/src/library/blast/subst_action.cpp
index 8bc919b88..406858dee 100644
--- a/src/library/blast/subst_action.cpp
+++ b/src/library/blast/subst_action.cpp
@@ -21,7 +21,7 @@ struct subst_proof_step_cell : public proof_step_cell {
         m_target(t), m_eq_href(e), m_rhs(r), m_dep(d) {}
     virtual ~subst_proof_step_cell() {}
 
-    virtual action_result resolve(expr const & pr) const {
+    virtual action_result resolve(expr const & pr) const override {
         try {
             state & s = curr_state();
             app_builder & b = get_app_builder();