diff options
| author | Pierre-Marie Pédrot | 2019-07-14 13:53:25 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-07-14 13:53:25 +0200 |
| commit | 76dfd0b95a7fd2de99f65de9fc10925d58777cd4 (patch) | |
| tree | 9a80f38a78b75d21b0fdd84b0a0f54a767adc290 /proofs/proof.ml | |
| parent | 3bd2722fb53552f45a25e6bc0a03a9ab0517485f (diff) | |
| parent | 2576fee1798b753161a730244c8d4d701e8a4641 (diff) | |
Merge PR #10496: [proof] Minor cleanup in proof.ml
Reviewed-by: ppedrot
Diffstat (limited to 'proofs/proof.ml')
| -rw-r--r-- | proofs/proof.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml index 9f2c90c375..5f07cc1acc 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -398,8 +398,6 @@ let run_tactic env tac pr = (*** Commands ***) -let in_proof p k = k (Proofview.return p.proofview) - (* Remove all the goals from the shelf and adds them at the end of the focused goals. *) let unshelve p = |