From 3b93c6cfbb838bcc2b9bdc1e4e2e669a86c75893 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 6 Dec 2014 16:31:22 +0100
Subject: Exporting store of goals so that new_evar in convert, intro, etc. can
 propagate it. This allows C-zar to continue to work.

Don't know if it is the best way to do it.
---
 proofs/proofview.ml  | 1 +
 proofs/proofview.mli | 1 +
 2 files changed, 2 insertions(+)

(limited to 'proofs')

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 08a43737c4..ff0e57be2b 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -856,6 +856,7 @@ module Goal = struct
   let sigma { sigma=sigma } = sigma
   let hyps { env=env } = Environ.named_context env
   let concl { concl=concl } = concl
+  let extra { sigma=sigma; self=self } = Goal.V82.extra sigma self
 
   let raw_concl { concl=concl } = concl
 
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index b758559beb..7e755d23d6 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -433,6 +433,7 @@ module Goal : sig
   val hyps : [ `NF ] t -> Context.named_context
   val env : 'a t -> Environ.env
   val sigma : 'a t -> Evd.evar_map
+  val extra : 'a t -> Evd.Store.t
 
   (** Returns the goal's conclusion even if the goal is not
       normalised. *)
-- 
cgit v1.2.3