diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/goal.ml | 2 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index 75f56c6b9d..a141708c2b 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -78,7 +78,7 @@ module V82 = struct let evars = Sigma.to_evar_map evars in let evars = Evd.restore_future_goals evars prev_future_goals prev_principal_goal in let ctxt = Environ.named_context_of_val hyps in - let inst = Array.map_of_list (mkVar % NamedDecl.get_id) ctxt in + let inst = Array.map_of_list (NamedDecl.get_id %> mkVar) ctxt in let ev = Term.mkEvar (evk,inst) in (evk, ev, evars) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index e900240761..93e276f4ba 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -103,7 +103,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 = pf_whd_all gls % pf_get_type_of gls +let pf_hnf_type_of gls = pf_get_type_of gls %> pf_whd_all gls let pf_is_matching = pf_apply Constr_matching.is_matching_conv let pf_matches = pf_apply Constr_matching.matches_conv |