diff options
Diffstat (limited to 'proofs/tacmach.ml')
| -rw-r--r-- | proofs/tacmach.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 4b027a127..97c5cda77 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -41,10 +41,8 @@ let project = Refiner.project let pf_env = Refiner.pf_env let pf_hyps = Refiner.pf_hyps -let test_conversion cb env sigma c1 c2 = - let c1 = EConstr.Unsafe.to_constr c1 in - let c2 = EConstr.Unsafe.to_constr c2 in - test_conversion cb env sigma c1 c2 +let test_conversion env sigma pb c1 c2 = + Reductionops.check_conv ~pb env sigma c1 c2 let pf_concl gls = Goal.V82.concl (project gls) (sig_it gls) let pf_hyps_types gls = |