diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-25 14:14:19 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-25 14:14:19 +0000 |
| commit | d284deddaf736d2387a79b219f328915bc12614c (patch) | |
| tree | c335d0d3de81f75bdb93b5cf6b2a033d51b6475a /ide/wg_Command.ml | |
| parent | db7b19f0f1d6b18bcc62fbedccad7a56f72315f2 (diff) | |
raise UnsafeSuccess -> feedback AddedAxiom
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16452 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/wg_Command.ml')
| -rw-r--r-- | ide/wg_Command.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index dd8896cba..ec759b67f 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.ml @@ -117,7 +117,7 @@ object(self) | Interface.Fail (l,str) -> result#buffer#insert ("Error while interpreting "^phrase^":\n"^str); Coq.return () - | Interface.Good res | Interface.Unsafe res -> + | Interface.Good res -> result#buffer#insert ("Result for command " ^ phrase ^ ":\n" ^ res); Coq.return ()) in |