diff options
| author | Enrico Tassi | 2015-07-30 10:41:13 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2015-07-30 14:35:20 +0200 |
| commit | 5d0ff1782ab54914e7b0e5a736922aa297d327c8 (patch) | |
| tree | e64ab53c43319fbf9de81c8f7a778460e434cd28 | |
| parent | 15a23fc7c103ba47d3f5e77853ff515d926573ca (diff) | |
STM: emit a warning when a QED/Admitted proof contains a nested lemma
| -rw-r--r-- | stm/stm.ml | 5 |
1 files changed, 4 insertions, 1 deletions
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) |