diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-16 10:10:02 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-16 10:37:47 +0200 |
| commit | e6708590ce648921f27395ce535e35d52aa2cc0f (patch) | |
| tree | d086ca3b9d6d98627290411be747d541dd15ee01 | |
| parent | 0ae6d27680e5b87bbb00c6941cee1b0c309624ec (diff) | |
Proofview: remove unused [refresh_sigma] compatibility primitive.
| -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 30c763ac1..cdc0c5e65 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 90a1b9fba..6d68cf4d4 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, |