diff options
| author | Enrico Tassi | 2013-12-24 18:12:26 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2013-12-24 18:23:41 +0100 |
| commit | 7a7dd14e763d13887101834fc2288046740cb8a2 (patch) | |
| tree | fe37d183be114e7b907629d60fb9d9ee7efb0683 /toplevel | |
| parent | 29969434c2b5625273e742d01cd7662c9db47d11 (diff) | |
CoqIDE: new feedback "incomplete" to signal partial Qed
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/stm.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/stm.ml b/toplevel/stm.ml index d05fce8b69..bca2ce24c5 100644 --- a/toplevel/stm.ml +++ b/toplevel/stm.ml @@ -1139,7 +1139,8 @@ let known_state ?(redefine_qed=false) ~cache id = qed.fproof <- Some (fp, cancel); let proof = Proof_global.close_future_proof fp in reach view.next; - vernac_interp id ~proof x + vernac_interp id ~proof x; + feedback ~state_id:id Interface.Incomplete | VtDrop, _, _ -> reach view.next; Option.iter (vernac_interp start) proof_using_ast; |