From 5d0ff1782ab54914e7b0e5a736922aa297d327c8 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 30 Jul 2015 10:41:13 +0200
Subject: STM: emit a warning when a QED/Admitted proof contains a nested lemma

---
 stm/stm.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index b6c6d41879..ee12e48d5d 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1688,7 +1688,10 @@ 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, None, accn, name, delegate name)
-    | `Sideff _ -> `Sync (no_name,None,`NestedProof)
+    | `Sideff _ ->
+        Pp.(msg_warning (strbrk ("Nested proofs are deprecated and will "^
+           "stop working in the next Coq version")));
+        `Sync (no_name,None,`NestedProof)
     | _ -> `Sync (no_name,None,`Unknown) in
  let make_sync why = function
    | `Sync(name,pua,_) -> `Sync (name,pua,why)
-- 
cgit v1.2.3