diff options
| -rw-r--r-- | proofs/proofview.ml | 3 | ||||
| -rw-r--r-- | proofs/proofview.mli | 3 |
2 files changed, 0 insertions, 6 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 30c763ac14..cdc0c5e658 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -977,9 +977,6 @@ module Goal = struct (* compatibility *) let goal { self=self } = self - let refresh_sigma g = - tclEVARMAP >>= fun sigma -> - tclUNIT { g with sigma } end diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 90a1b9fba9..6d68cf4d46 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -423,9 +423,6 @@ module Goal : sig (* compatibility: avoid if possible *) val goal : [ `NF ] t -> Goal.goal - (** [refresh g] updates the [sigma g] to the current value, may be - useful with compatibility functions like [Tacmach.New.of_old] *) - val refresh_sigma : 'a t -> 'a t tactic end (** A light interface for building tactics out of partial term. Be careful, |