diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-05-20 03:18:41 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-06-16 18:21:08 +0200 |
| commit | 677d5deb72734a0e5502bcf47a905fcdf9374e51 (patch) | |
| tree | c8812b98a4c5c2f34412b5d39a054be474679457 | |
| parent | 8d06718fd4d99f4e5bc33452a02ea27d5a9279ed (diff) | |
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.
| -rw-r--r-- | engine/proofview.ml | 7 | ||||
| -rw-r--r-- | engine/proofview.mli | 10 |
2 files changed, 17 insertions, 0 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml index b8f49a9c8..d87686065 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 diff --git a/engine/proofview.mli b/engine/proofview.mli index 0b63164b0..901cf26e0 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -300,6 +300,16 @@ val tclINDEPENDENT : unit tactic -> unit tactic shelf for later use (or being solved by side-effects). *) val shelve : unit tactic +(** Shelves the given list of goals, which might include some that are + under focus and some that aren't. All the goals are placed on the + shelf for later use (or being solved by side-effects). *) +val shelve_goals : Goal.goal list -> unit tactic + +(** [unifiable sigma g l] checks whether [g] appears in another + subgoal of [l]. The list [l] may contain [g], but it does not + affect the result. Used by [shelve_unifiable]. *) +val unifiable : Evd.evar_map -> Goal.goal -> Goal.goal list -> bool + (** Shelves the unifiable goals under focus, i.e. the goals which appear in other goals under focus (the unfocused goals are not considered). *) |