From 677d5deb72734a0e5502bcf47a905fcdf9374e51 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 20 May 2016 03:18:41 +0200
Subject: Proofview: extensions for backtracking eauto

unshelve_goals is used to correctly register dependent
subgoals that have to be solved. Resolution may fail to
do so using hints, so we have to put them back as goals
in that case. The shelf is a good interface for doing that.

unifiable can be used outside proofview to detect dependencies
between goals. This might be better in another module.
---
 engine/proofview.ml | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'engine/proofview.ml')

diff --git a/engine/proofview.ml b/engine/proofview.ml
index b8f49a9c84..d876860652 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -618,6 +618,13 @@ let shelve =
   InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve")) >>
   Shelf.modify (fun gls -> gls @ initial)
 
+let shelve_goals l =
+  let open Proof in
+  Comb.get >>= fun initial ->
+  let comb = CList.filter (fun g -> not (CList.mem g l)) initial in
+  Comb.set comb >>
+  InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve_goals")) >>
+  Shelf.modify (fun gls -> gls @ l)
 
 (** [contained_in_info e evi] checks whether the evar [e] appears in
     the hypotheses, the conclusion or the body of the evar_info
-- 
cgit v1.2.3