From 1ffa181c8015584fe1762a5ab8f6a664725767fa Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 9 May 2018 17:48:44 +0200 Subject: Remove deprecation warning for nested proofs. It is not clear yet that support for nested proofs will actually get removed in a future version. --- stm/stm.ml | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) (limited to 'stm') 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 -- cgit v1.2.3