diff options
| author | Arnaud Spiwack | 2014-09-15 16:46:08 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-09-15 17:17:35 +0200 |
| commit | 83ebacdb7f307451fc801637224c911eb0da9fea (patch) | |
| tree | b8677fbc66d6bef4c62cbbb8995ec585a704b6d3 /proofs/proofview.mli | |
| parent | 27e2e43b93491727096b9d1fb20f66cfc71ae320 (diff) | |
Fix timing of evar-normalisation of goals in [Ftactic.nf_enter].
All goals were normalised up front, rather than normalised after the tactic acting on previous goal had the chance to solve some evars, which then appeared non-instantiated to tactics which do not work up to evar map (most of them).
Diffstat (limited to 'proofs/proofview.mli')
| -rw-r--r-- | proofs/proofview.mli | 6 |
1 files changed, 3 insertions, 3 deletions
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 |