From ed54d13461631f07f545112d8b534fb1344029be Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 9 Nov 2003 12:52:48 +0000
Subject: Ajout pf_apply

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

diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index c7bc2a1d0b..32951721b5 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -98,7 +98,8 @@ let pf_execute gls =
 let pf_reduction_of_redexp gls re c = 
   reduction_of_redexp re (pf_env gls) (project gls) c 
 
-let pf_reduce redfun gls c       = redfun (pf_env gls) (project gls) c 
+let pf_apply f gls = f (pf_env gls) (project gls)
+let pf_reduce = pf_apply
 
 let pf_whd_betadeltaiota         = pf_reduce whd_betadeltaiota
 let pf_whd_betadeltaiota_stack   = pf_reduce whd_betadeltaiota_stack
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 931f988dd4..7031852f57 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -66,7 +66,7 @@ val pf_get_new_ids : identifier list -> goal sigma -> identifier list
 val pf_reduction_of_redexp : goal sigma -> red_expr -> constr -> constr
 
 
-
+val pf_apply : (env -> evar_map -> 'a) -> goal sigma -> 'a
 val pf_reduce : 
   (env -> evar_map -> constr -> constr) ->
     goal sigma -> constr -> constr
-- 
cgit v1.2.3