aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorgareuselesinge2013-09-12 12:45:20 +0000
committergareuselesinge2013-09-12 12:45:20 +0000
commit2de1c607e1e30a2d0057760fa4357e6adbe58c89 (patch)
tree79f529c746427c4ed5bbacc69824e3c8f01faf67
parente4ae7d3d2dc8751af52f86f3d785ea486139816f (diff)
Remove outdated comment
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16770 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--toplevel/vernac.ml13
1 files changed, 0 insertions, 13 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 6051b65a48..45c0f68135 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -269,19 +269,6 @@ let rec vernac_com verbosely checknav (loc,com) =
| v when !just_parsing -> ()
| v -> Stm.process_transaction verbosely (loc,v)
- (* FIXME elsewhere let rollback =
- if !Flags.batch_mode then States.without_rollback
- else States.with_heavy_rollback
- in
- let psh = default_set_timeout () in
- try
- rollback interpfun Cerrors.process_vernac_interp_error v;
- restore_timeout psh;
- with reraise ->
- let reraise = Errors.push reraise in
- restore_timeout psh;
- raise reraise
- *)
in
try
checknav loc com;