diff options
| author | Pierre-Marie Pédrot | 2020-05-12 12:13:50 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-12 12:18:19 +0200 |
| commit | 65551cdf811a1bf428fcdc7e3e5c51df0fffcb78 (patch) | |
| tree | 995028e052cf0e8b37214d18462dc1ce4c5e8067 /proofs/clenvtac.ml | |
| parent | d31cb4d3e55da99d42abdc1f4129ddc03e1631c6 (diff) | |
Wrap the legacy refiner type into the Logic API.
Diffstat (limited to 'proofs/clenvtac.ml')
| -rw-r--r-- | proofs/clenvtac.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 695e103082..c5e341c720 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -13,7 +13,6 @@ open Constr open Termops open Evd open EConstr -open Refiner open Logic open Reduction open Clenv |