diff options
| author | Pierre-Marie Pédrot | 2014-06-17 17:58:51 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-06-19 15:05:13 +0200 |
| commit | dbe87dc85d7bd1c7d597a7a6ee00ffc1b70948ad (patch) | |
| tree | 0437003cdcc2cee76c586dc24164c8a95bf50ae5 /proofs | |
| parent | 2a8e86e504e57d3c47d65fee408cec9aa9419445 (diff) | |
Adding a raw_goals primitive for Tacinterp.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proofview.ml | 14 | ||||
| -rw-r--r-- | proofs/proofview.mli | 3 |
2 files changed, 17 insertions, 0 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index c8983700f9..c478bd6635 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -838,6 +838,20 @@ module Goal = struct in tclUNIT (List.map_filter map step.comb) + let raw_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 (raw_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 f959513d42..6a2d815114 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -376,6 +376,9 @@ module Goal : sig (** Recover the list of current goals under focus *) val goals : [ `NF ] t list tactic + (** Recover the list of current goals under focus, without evar-normalization *) + val raw_goals : [ `LZ ] t list tactic + (* compatibility: avoid if possible *) val goal : [ `NF ] t -> Goal.goal |