From b4e4c4d6106c77c2e07b7ec3fa4310b82eddd990 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 27 Jun 2014 07:02:13 -0700 Subject: [PATCH] chore(library/tactic): remove unnecessary file Signed-off-by: Leonardo de Moura --- src/library/tactic/assignment.h | 20 -------------------- 1 file changed, 20 deletions(-) delete mode 100644 src/library/tactic/assignment.h diff --git a/src/library/tactic/assignment.h b/src/library/tactic/assignment.h deleted file mode 100644 index 264177f5f..000000000 --- a/src/library/tactic/assignment.h +++ /dev/null @@ -1,20 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include "kernel/metavar.h" - -namespace lean { -/** - \brief Wrapper for metavar_env that only allows us to access the assignment. -*/ -class assignment { - metavar_env m_menv; -public: - assignment(metavar_env const & menv):m_menv(menv) {} - optional operator()(name const & mvar) const { return m_menv->get_subst(mvar); } -}; -}