diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proofview.ml | 8 | ||||
| -rw-r--r-- | proofs/proofview.mli | 2 |
2 files changed, 7 insertions, 3 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 75725e47c4..6ecf4da7e6 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -942,8 +942,12 @@ module Goal = struct 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 + let gl = + tclEVARMAP >>= fun sigma -> + (** The sigma is unchanged. *) + let (gl, _) = Goal.eval (enter_t (fun gl -> gl)) env sigma goal in + tclUNIT gl + in Some gl in tclUNIT (List.map_filter map step.comb) diff --git a/proofs/proofview.mli b/proofs/proofview.mli index bda88178bf..c44707c1e7 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -416,7 +416,7 @@ module Goal : sig val enter : ([ `LZ ] t -> unit tactic) -> unit tactic (** Recover the list of current goals under focus, without evar-normalization *) - val goals : [ `LZ ] t list tactic + val goals : [ `LZ ] t tactic list tactic (* compatibility: avoid if possible *) val goal : [ `NF ] t -> Goal.goal |