From 060c10020b7fce5d47de7a882cff335779c6888e Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Wed, 18 Apr 2012 14:47:34 +0000
Subject: Two dead functions in Tacmach.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15202 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/tacmach.ml  | 8 --------
 proofs/tacmach.mli | 3 ---
 2 files changed, 11 deletions(-)

diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 75e9cdf62a..58d72d4b29 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -73,14 +73,6 @@ let pf_get_new_ids ids gls =
     (fun id acc -> (next_ident_away id (acc@avoid))::acc)
     ids []
 
-let pf_interp_constr gls c =
-  let evc = project gls in
-  Constrintern.interp_constr evc (pf_env gls) c
-
-let pf_interp_type gls c =
-  let evc = project gls in
-  Constrintern.interp_type evc (pf_env gls) c
-
 let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id
 
 let pf_parse_const gls = compose (pf_global gls) id_of_string
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 884a030703..402002de16 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -48,9 +48,6 @@ val pf_type_of            : goal sigma -> constr -> types
 val pf_check_type         : goal sigma -> constr -> types -> unit
 val pf_hnf_type_of        : goal sigma -> constr -> types
 
-val pf_interp_constr      : goal sigma -> Topconstr.constr_expr -> constr
-val pf_interp_type        : goal sigma -> Topconstr.constr_expr -> types
-
 val pf_get_hyp            : goal sigma -> identifier -> named_declaration
 val pf_get_hyp_typ        : goal sigma -> identifier -> types
 
-- 
cgit v1.2.3