diff options
| -rw-r--r-- | proofs/proofview.ml | 8 | ||||
| -rw-r--r-- | proofs/proofview.mli | 2 | ||||
| -rw-r--r-- | tactics/ftactic.ml | 3 |
3 files changed, 9 insertions, 4 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 diff --git a/tactics/ftactic.ml b/tactics/ftactic.ml index 43602d1fb6..d8b12fc4e4 100644 --- a/tactics/ftactic.ml +++ b/tactics/ftactic.ml @@ -40,12 +40,13 @@ let bind (type a) (type b) (m : a t) (f : a -> b t) : b t = m >>= function let nf_enter f = bind (Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l)) (fun gl -> + gl >>= fun gl -> Proofview.Goal.normalize gl >>= fun nfgl -> Proofview.V82.wrap_exceptions (fun () -> f nfgl)) let enter f = bind (Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l)) - (fun gl -> Proofview.V82.wrap_exceptions (fun () -> f gl)) + (fun gl -> gl >>= fun gl -> Proofview.V82.wrap_exceptions (fun () -> f gl)) let lift (type a) (t:a Proofview.tactic) : a t = Proofview.tclBIND t (fun x -> Proofview.tclUNIT (Uniform x)) |