diff options
| author | Pierre-Marie Pédrot | 2020-01-28 13:31:51 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-01-28 13:31:51 +0100 |
| commit | b105077dd42e34f19d0849620fec2837e84b4887 (patch) | |
| tree | 217628a17b0d335d8ad453bf7bab34a2b68227fe /toplevel | |
| parent | 36c61df9435ce382084ddb097ffe0c7b2e220cbb (diff) | |
| parent | c825bc9caf3abb9610310b79f9420688f06bdf54 (diff) | |
Merge PR #11379: [ocaml] Remove Custom Backtrace module in favor of OCaml's
Reviewed-by: ppedrot
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqargs.ml | 2 | ||||
| -rw-r--r-- | toplevel/coqinit.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 56a6312b61..52e2562ae8 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -513,7 +513,7 @@ let parse_args ~help ~init arglist : t * string list = }}} |"-test-mode" -> Vernacinterp.test_mode := true; oval |"-beautify" -> Flags.beautify := true; oval - |"-bt" -> Backtrace.record_backtrace true; oval + |"-bt" -> Exninfo.record_backtrace true; oval |"-color" -> set_color oval (next ()) |"-config"|"--config" -> set_query oval PrintConfig |"-debug" -> Coqinit.set_debug (); oval diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index ae37e40101..ac348b9646 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -14,7 +14,7 @@ open Pp let ( / ) s1 s2 = Filename.concat s1 s2 let set_debug () = - let () = Backtrace.record_backtrace true in + let () = Exninfo.record_backtrace true in Flags.debug := true (* Loading of the resource file. diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index bca6b48499..adcce67b0d 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -69,10 +69,10 @@ let interp_vernac ~check ~interactive ~state ({CAst.loc;_} as com) = let new_proof = Vernacstate.Proof_global.give_me_the_proof_opt () [@ocaml.warning "-3"] in { state with doc = ndoc; sid = nsid; proof = new_proof; } with reraise -> + let (reraise, info) = CErrors.push reraise in (* XXX: In non-interactive mode edit_at seems to do very weird things, so we better avoid it while we investigate *) if interactive then ignore(Stm.edit_at ~doc:state.doc state.sid); - let (reraise, info) = CErrors.push reraise in let info = begin match Loc.get_loc info with | None -> Option.cata (Loc.add_loc info) info loc |