diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-19 18:16:23 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-19 18:16:23 +0000 |
| commit | 51684142c40fced940bb870742bc7f75c3e2fd52 (patch) | |
| tree | 9a8e883e7c53d2fa23ef8f0d9deffabeccfeb56e /toplevel/toplevel.ml | |
| parent | 09d7951e0c0009e4ac55091cede25b88576759d2 (diff) | |
Modulification and removing of structural equality in Stateid.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16705 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/toplevel.ml')
| -rw-r--r-- | toplevel/toplevel.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index eb9f4a03d..da3049141 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -213,7 +213,7 @@ let make_prompt () = "n |lem1|lem2|lem3| p < " *) let make_emacs_prompt() = - let statnum = Stateid.string_of_state_id (Stm.get_current_state ()) in + let statnum = Stateid.to_string (Stm.get_current_state ()) in let dpth = Stm.current_proof_depth() in let pending = Stm.get_all_proof_names() in let pendingprompt = @@ -319,9 +319,9 @@ let do_vernac () = Format.set_formatter_out_channel stdout; ppnl (print_toplevel_error any); pp_flush (); - match Stateid.get_state_id any with + match Stateid.get any with | Some (valid_id,_) -> - let valid = Stateid.int_of_state_id valid_id in + let valid = Stateid.to_int valid_id in Vernac.eval_expr (Loc.ghost, (Vernacexpr.VernacStm (Vernacexpr.Command (Vernacexpr.VernacBackTo valid)))) @@ -336,7 +336,7 @@ let do_vernac () = let feed_emacs = function | { Interface.id = Interface.State id; Interface.content = Interface.GlobRef (_,a,_,c,_) } -> - prerr_endline ("<info>" ^"<id>"^Stateid.string_of_state_id id ^"</id>" + prerr_endline ("<info>" ^"<id>"^Stateid.to_string id ^"</id>" ^a^" "^c^ "</info>") | _ -> () |