From b853c8433ca4d06bc23e6162dcba44187330a1a0 Mon Sep 17 00:00:00 2001
From: Nishant Rodrigues <nishantjr@gmail.com>
Date: Mon, 20 Apr 2020 23:05:54 +0530
Subject: [PATCH] core: cool sequences back in, so that subgoals are only
 generated for a single uncomposed strategy

---
 prover/strategies/core.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/prover/strategies/core.md b/prover/strategies/core.md
index 4b330da04..77878fbb8 100644
--- a/prover/strategies/core.md
+++ b/prover/strategies/core.md
@@ -67,6 +67,8 @@ cooled back into the sequence strategy.
        <trace> _ => S1 </trace>
     requires notBool(isResultStrategy(S1))
      andBool notBool(isSequenceStrategy(S1))
+  rule <claim> GOAL:Pattern </claim>
+       <strategy> S1:SequenceStrategy ~> #hole . S2 => S1 . S2 </strategy>
   rule <claim> GOAL:Pattern </claim>
        <strategy> S1:ResultStrategy ~> #hole . S2 => subgoal(GOAL, S1 . S2) </strategy>
 ```