From e6708590ce648921f27395ce535e35d52aa2cc0f Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack <arnaud@spiwack.net>
Date: Thu, 16 Oct 2014 10:10:02 +0200
Subject: Proofview: remove unused [refresh_sigma] compatibility primitive.

---
 proofs/proofview.ml  | 3 ---
 proofs/proofview.mli | 3 ---
 2 files changed, 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,
-- 
cgit v1.2.3