From d976efa0b6cfd4be2aa1d9bf8da5a4b266873b15 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 27 Mar 2014 20:04:24 +0100
Subject: Removing tactic compatibility layer from Eqdecide.

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

(limited to 'proofs')

diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index fcba8119d2..fbe201f1a3 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -274,6 +274,7 @@ module New = struct
   let pf_matches gl pat t = pf_apply ConstrMatching.matches_conv gl pat t
 
   let pf_whd_betadeltaiota gl t = pf_apply whd_betadeltaiota gl t
+  let pf_compute gl t = pf_apply compute gl t
 
   let pf_nf_evar gl t = nf_evar (Proofview.Goal.sigma gl) t
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index d122b09417..897073f36b 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -152,6 +152,7 @@ module New : sig
   val pf_hnf_type_of : 'a Proofview.Goal.t -> constr -> types
 
   val pf_whd_betadeltaiota : 'a Proofview.Goal.t -> constr -> constr
+  val pf_compute : 'a Proofview.Goal.t -> constr -> constr
 
   val pf_matches : 'a Proofview.Goal.t -> constr_pattern -> constr -> patvar_map
 
-- 
cgit v1.2.3