diff options
| author | courtieu | 2006-12-28 15:41:39 +0000 |
|---|---|---|
| committer | courtieu | 2006-12-28 15:41:39 +0000 |
| commit | d556fd3ffb8b59e2a5136ab748a3a8d73c3f45f0 (patch) | |
| tree | df77fe692c2176defbb5414b2448af9e243cd08b /toplevel | |
| parent | 76f02a4751c3eac40d91dfa7bb61de1f985672d3 (diff) | |
Cleaning backtracking code, optimized "Backtrack n x y" when n is
current state.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9464 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernac.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 185bfd93c8..4090748b3b 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -195,8 +195,8 @@ and read_vernac_file verbosely s = (* raw_do_vernac : char Stream.t -> unit * parses and executes one command of the vernacular char stream. - * Marks the end of the command in the lib_stk to make vernac undoing - * easier. *) + * Marks the end of the command in the lib_stk with a new label to + * make vernac undoing easier. *) let raw_do_vernac po = vernac (States.with_heavy_rollback Vernacentries.interp) (po,None); |