From 4c6a5f56ef5ab248d9e816b4d7bee3001cab9a2e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 3 Apr 2014 15:55:27 +0200
Subject: Removing tactic compatibility layer from Elim.

---
 proofs/tacmach.ml  | 1 +
 proofs/tacmach.mli | 2 ++
 2 files changed, 3 insertions(+)

(limited to 'proofs')

diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 72a1287ec9..0f898feef2 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -202,6 +202,7 @@ module New = struct
     let hyps = Proofview.Goal.hyps gl in
     Constrintern.construct_reference hyps id
 
+  let pf_env = Proofview.Goal.env
 
   let pf_type_of gl t =
     pf_apply type_of gl t
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index a840dd15aa..6e48908078 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -122,6 +122,8 @@ module New : sig
   val pf_global : identifier -> 'a Proofview.Goal.t -> constr
   val of_old : (Proof_type.goal Evd.sigma -> 'a) -> [ `NF ] Proofview.Goal.t -> 'a
 
+  val pf_env : 'a Proofview.Goal.t -> Environ.env
+
   val pf_type_of : 'a Proofview.Goal.t -> Term.constr -> Term.types
   val pf_get_type_of : 'a Proofview.Goal.t -> Term.constr -> Term.types
   val pf_conv_x : 'a Proofview.Goal.t -> Term.constr -> Term.constr -> bool
-- 
cgit v1.2.3