diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-24 17:15:15 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:38 +0100 |
| commit | 531590c223af42c07a93142ab0cea470a98964e6 (patch) | |
| tree | bfe531d8d32e491a66eceba60995702e20e73757 /proofs/tacmach.ml | |
| parent | b36adb2124d3ba8a5547605e7f89bb0835d0ab10 (diff) | |
Removing compatibility layers in Retyping
Diffstat (limited to 'proofs/tacmach.ml')
| -rw-r--r-- | proofs/tacmach.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index d9caadd54..7ffb30fa8 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -108,7 +108,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_get_type_of gls %> EConstr.of_constr %> pf_whd_all gls +let pf_hnf_type_of gls = pf_get_type_of gls %> pf_whd_all gls let pf_is_matching gl p c = pf_apply Constr_matching.is_matching_conv gl p c let pf_matches gl p c = pf_apply Constr_matching.matches_conv gl p c @@ -234,7 +234,7 @@ module New = struct let pf_hnf_constr gl t = pf_apply hnf_constr gl t let pf_hnf_type_of gl t = - pf_whd_all gl (EConstr.of_constr (pf_get_type_of gl t)) + pf_whd_all gl (pf_get_type_of gl t) let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t |