From e2540b68db76d29cbfe1385c5fcdd8bcfd00fe06 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 28 Jan 2014 15:56:01 -0800
Subject: [PATCH] fix(src/builtin/tactic): add default rule set if none is
 provided

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

diff --git a/src/builtin/tactic.lua b/src/builtin/tactic.lua
index 5d5eef9148..1d56b29911 100644
--- a/src/builtin/tactic.lua
+++ b/src/builtin/tactic.lua
@@ -19,6 +19,9 @@ tactic_macro("unfold", { macro_arg.Id }, function (env, id) return unfold_tac(id
 
 tactic_macro("simp", { macro_arg.Ids },
              function (env, ids)
+                if #ids == 0 then
+                   ids[1] = "default"
+                end
                 return simp_tac(ids)
              end
 )