diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proofview.ml | 20 | ||||
| -rw-r--r-- | proofs/proofview.mli | 6 |
2 files changed, 9 insertions, 17 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index a97add1ce7..75725e47c4 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -911,6 +911,12 @@ module Goal = struct tclZERO e end + let normalize { self } = + Proof.current >>= fun env -> + tclEVARMAP >>= fun sigma -> + let (gl,sigma) = Goal.eval nf_enter_t env sigma self in + tclTHEN (V82.tclEVARS sigma) (tclUNIT gl) + let enter_t f = Goal.enter begin fun env sigma concl self -> f {env=env;sigma=sigma;concl=concl;self=self} end @@ -928,20 +934,6 @@ module Goal = struct tclZERO e end - let nf_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 nf_enter_t env sigma goal in - Some gl - in - tclUNIT (List.map_filter map step.comb) - let goals = Proof.current >>= fun env -> Proof.get >>= fun step -> diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 94969f3a5c..bda88178bf 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -395,6 +395,9 @@ module Goal : sig (** Assume that you do not need the goal to be normalized. *) val assume : 'a t -> [ `NF ] t + (** Normalises the argument goal. *) + val normalize : 'a t -> [ `NF ] t tactic + (* [concl], [hyps], [env] and [sigma] given a goal [gl] return respectively the conclusion of [gl], the hypotheses of [gl], the environment of [gl] (i.e. the global environment and the hypotheses) @@ -412,9 +415,6 @@ module Goal : sig (** Same as nf_enter, but does not normalize the goal beforehand. *) val enter : ([ `LZ ] t -> unit tactic) -> unit tactic - (** Recover the list of current goals under focus *) - val nf_goals : [ `NF ] t list tactic - (** Recover the list of current goals under focus, without evar-normalization *) val goals : [ `LZ ] t list tactic |