diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-05-09 17:48:44 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-05-17 10:36:33 +0200 |
| commit | 1ffa181c8015584fe1762a5ab8f6a664725767fa (patch) | |
| tree | 2aad81d9b599721ef72a7d927a7e68a5ddb4bf1f /stm | |
| parent | 49d73185be33ce521f4664e61d47b2db5d59d608 (diff) | |
Remove deprecation warning for nested proofs.
It is not clear yet that support for nested proofs will actually get removed in a future version.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 9 |
1 files changed, 1 insertions, 8 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 90360dce9..9192c1410 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2113,12 +2113,6 @@ let delegate name = || VCS.is_vio_doc () || !cur_opt.async_proofs_full -let warn_deprecated_nested_proofs = - CWarnings.create ~name:"deprecated-nested-proofs" ~category:"deprecated" - (fun () -> - strbrk ("Nested proofs are deprecated and will "^ - "stop working in a future Coq version")) - let collect_proof keep cur hd brkind id = stm_prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id); let no_name = "" in @@ -2200,8 +2194,7 @@ let collect_proof keep cur hd brkind id = assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch); let name = name ids in `MaybeASync (parent last, accn, name, delegate name) - | `Sideff _ -> - warn_deprecated_nested_proofs (); + | `Sideff (CherryPickEnv,_) -> `Sync (no_name,`NestedProof) | _ -> `Sync (no_name,`Unknown) in let make_sync why = function |