diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 9b626d8bcf..1ce0e27a18 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -303,6 +303,15 @@ let _ = | [] -> (fun () -> abort_refine Lib.reset_initial ()) | _ -> bad_vernac_args "ResetInitial") +let _ = + add "Back" + (function + | [] -> (fun () -> Lib.back 1) + | [VARG_NUMBER n] -> + if n < 1 then error "argument of Back must be positive" + else (fun () -> Lib.back n) + | _ -> bad_vernac_args "Back") + (*** let _ = add "ResetSection" |