From b119c11473c1a0fd8646133fdf660e1068524994 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 9 Feb 2014 20:28:30 -0800
Subject: [PATCH] feat(builtin/tactic): add simp_no_assump tactic

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/builtin/tactic.lua | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/src/builtin/tactic.lua b/src/builtin/tactic.lua
index 436157449..c7f852e3b 100644
--- a/src/builtin/tactic.lua
+++ b/src/builtin/tactic.lua
@@ -27,6 +27,15 @@ tactic_macro("simp", { macro_arg.Ids },
              end
 )
 
+tactic_macro("simp_no_assump", { macro_arg.Ids },
+             function (env, ids)
+                if #ids == 0 then
+                   ids[1] = "default"
+                end
+                return simp_tac(ids, options({"simp_tac", "assumptions"}, false))
+             end
+)
+
 -- Create a 'bogus' tactic that consume all goals, but it does not create a valid proof.
 -- This tactic is useful for momentarily ignoring/skipping a "hole" in a big proof.
 -- Remark: the kernel will not accept a proof built using this tactic.