diff options
| author | Emilio Jesus Gallego Arias | 2019-05-28 02:48:42 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-05-29 02:17:16 +0200 |
| commit | 4d2cba0876a95734d69ceef71f4a553c80737b5e (patch) | |
| tree | 69e6bd6b2bef2709d4ed5e392edd63d0239b5a50 /proofs/refine.ml | |
| parent | 09514118c386420650847ba74c7f985bb0a05776 (diff) | |
[proofs] Remove unused API [detected by coverage]
We remove unused parts of the API, almost all of them belonging to the
legacy engine. This was detected using coverage testing.
The list is provisional and should be subject to change, let's see
what CI says.
Diffstat (limited to 'proofs/refine.ml')
| -rw-r--r-- | proofs/refine.ml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/proofs/refine.ml b/proofs/refine.ml index 4a9404aa96..8439156e65 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -116,9 +116,6 @@ let lift c = let make_refine_enter ~typecheck f gl = generic_refine ~typecheck (lift f) gl -let refine_one ~typecheck f = - Proofview.Goal.enter_one (make_refine_enter ~typecheck f) - let refine ~typecheck f = let f evd = let (evd,c) = f evd in (evd,((), c)) |