diff options
Diffstat (limited to 'proofs/tacmach.ml')
| -rw-r--r-- | proofs/tacmach.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index a10d8fd2f..1e59c182c 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -99,7 +99,7 @@ let pf_const_value = pf_reduce (fun env _ -> constant_value_in 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 pf_hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_get_type_of gls) +let pf_hnf_type_of gls = pf_whd_betadeltaiota gls % pf_get_type_of gls let pf_is_matching = pf_apply Constr_matching.is_matching_conv let pf_matches = pf_apply Constr_matching.matches_conv |