diff options
| author | herbelin | 2003-11-09 12:52:48 +0000 |
|---|---|---|
| committer | herbelin | 2003-11-09 12:52:48 +0000 |
| commit | ed54d13461631f07f545112d8b534fb1344029be (patch) | |
| tree | b0a24ca541a6f6f18eed5094edeae4182140f67f /proofs | |
| parent | 426767b93914a2d2347eff6c7dbc6d22e5be36ef (diff) | |
Ajout pf_apply
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4836 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/tacmach.ml | 3 | ||||
| -rw-r--r-- | 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 |