diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-03-14 21:29:19 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-03-14 21:29:19 +0000 |
| commit | 208f162ab68d00488248ee052947592dd23d5d52 (patch) | |
| tree | 4009b4e1da390933e5ccfc878390478041c6679a /proofs/tacmach.ml | |
| parent | 4b7200cbbf4f2462d6f1398a191377b4d57f7655 (diff) | |
Cleaning/uniformizing the interface of tacticals.mli
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11980 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/tacmach.ml')
| -rw-r--r-- | proofs/tacmach.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index f9b7b8677..fa22de7bb 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -111,11 +111,14 @@ let pf_const_value = pf_reduce (fun env _ -> constant_value env) let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind -let hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_get_type_of gls) +let pf_hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_get_type_of gls) let pf_check_type gls c1 c2 = ignore (pf_type_of gls (mkCast (c1, DEFAULTcast, c2))) +let pf_is_matching = pf_apply Matching.is_matching_conv +let pf_matches = pf_apply Matching.matches_conv + (************************************) (* Tactics handling a list of goals *) (************************************) |