diff options
| author | Pierre-Marie Pédrot | 2014-05-23 18:41:47 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-06-03 01:20:36 +0200 |
| commit | 259ec71685cf2180403e35acea32cb42ba6b761b (patch) | |
| tree | 20364037953979d99e722591d2445fe5aa144b78 /proofs | |
| parent | 2e3f59f8d689b45fcad8cfd0f3dc1d5e693d8546 (diff) | |
The tactic interpreter now uses a new type of tactics, through
the GTac module. A ['a Gtac.t] is a special case of tactic that
may depend on the current goals, or not. Internally, it construct
a list of results, one for each focussed goal, if the tactic is
actually dependent.
This allows for an interpretation of whole-goal tactic that does
work, which was not the case for the previous implementation,
which did to many Proofview.Goal.enter.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proofview.ml | 14 | ||||
| -rw-r--r-- | proofs/proofview.mli | 4 |
2 files changed, 18 insertions, 0 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 6651e49652..eaaa1f7c30 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -826,6 +826,20 @@ module Goal = struct tclZERO e end + let goals = + Proof.current >>= fun env -> + Proof.get >>= fun step -> + let sigma = step.solution in + let map goal = + match Goal.advance sigma goal with + | None -> None (** ppedrot: Is this check really necessary? *) + | Some goal -> + (** The sigma is unchanged. *) + let (gl, _) = Goal.eval (enter_t (fun gl -> gl)) env sigma goal in + Some gl + in + tclUNIT (List.map_filter map step.comb) + (* compatibility *) let goal { self=self } = self let refresh_sigma g = diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 6177803c78..c27e4ba1a9 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -370,8 +370,12 @@ module Goal : sig each goal. *) val enter : ([ `NF ] t -> unit tactic) -> unit tactic + (** Same as enter, but does not normalize the goal beforehand. *) val raw_enter : ([ `LZ ] t -> unit tactic) -> unit tactic + (** Recover the list of current goals under focus *) + val goals : [ `NF ] t list tactic + (* compatibility: avoid if possible *) val goal : [ `NF ] t -> Goal.goal |