From 6541e32be7018104c47ccad75ff41ffc750ff944 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 27 Apr 2014 23:26:14 +0200
Subject: Rewriting [lapply] tactic in the new monad.

---
 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 a36b7f2ac4..855529ac28 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -243,6 +243,7 @@ module New = struct
   let pf_reduce_to_quantified_ind gl t =
     pf_apply reduce_to_quantified_ind gl t
 
+  let pf_hnf_constr gl t = pf_apply hnf_constr gl t
   let pf_hnf_type_of gl t =
     pf_whd_betadeltaiota gl (pf_get_type_of gl t)
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 92f8ef8293..7bac4c6e9e 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -127,6 +127,7 @@ module New : sig
   val pf_nf_concl : [ `LZ ] Proofview.Goal.t -> types
   val pf_reduce_to_quantified_ind : 'a Proofview.Goal.t -> types -> inductive * types
 
+  val pf_hnf_constr : 'a Proofview.Goal.t -> constr -> types
   val pf_hnf_type_of : 'a Proofview.Goal.t -> constr -> types
 
   val pf_whd_betadeltaiota : 'a Proofview.Goal.t -> constr -> constr
-- 
cgit v1.2.3