diff options
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)) |