diff options
| author | Pierre-Marie Pédrot | 2017-09-04 19:14:30 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-04 19:20:23 +0200 |
| commit | 567435828772e53327bacf7464291a5759c23831 (patch) | |
| tree | 383e7ba91b9b119cb1fc281fc36bcc38ca82e582 /src | |
| parent | d80e854d6827252676c2c504bb3108152a94d629 (diff) | |
Better backtraces for a few datatypes.
Diffstat (limited to 'src')
| -rw-r--r-- | src/tac2core.ml | 8 | ||||
| -rw-r--r-- | src/tac2entries.ml | 9 |
2 files changed, 11 insertions, 6 deletions
diff --git a/src/tac2core.ml b/src/tac2core.ml index 17fa7c28f4..e4bd80adc8 100644 --- a/src/tac2core.ml +++ b/src/tac2core.ml @@ -930,9 +930,13 @@ let () = let _, tac = Genintern.intern Ltac_plugin.Tacarg.wit_tactic ist tac in GlbVal tac, gtypref t_unit in - let interp _ tac = + let interp ist tac = + let ist = { ist with env_ist = Id.Map.empty } in + let lfun = Tac2interp.set_env ist Id.Map.empty in + let ist = Ltac_plugin.Tacinterp.default_ist () in (** FUCK YOU API *) - (Obj.magic Ltac_plugin.Tacinterp.eval_tactic tac : unit Proofview.tactic) >>= fun () -> + let ist = { ist with API.Geninterp.lfun = (Obj.magic lfun) } in + (Obj.magic Ltac_plugin.Tacinterp.eval_tactic_ist ist tac : unit Proofview.tactic) >>= fun () -> return v_unit in let subst s tac = Genintern.substitute Ltac_plugin.Tacarg.wit_tactic s tac in diff --git a/src/tac2entries.ml b/src/tac2entries.ml index 8d515577ec..197ec19b3a 100644 --- a/src/tac2entries.ml +++ b/src/tac2entries.ml @@ -756,14 +756,15 @@ let _ = Goptions.declare_bool_option { } let pr_frame = function -| FrLtac None -> str "<anonymous>" +| FrLtac None -> str "Call <anonymous>" | FrLtac (Some kn) -> - Libnames.pr_qualid (Tac2env.shortest_qualid_of_ltac (TacConstant kn)) + str "Call " ++ Libnames.pr_qualid (Tac2env.shortest_qualid_of_ltac (TacConstant kn)) | FrPrim ml -> - str "<" ++ str ml.mltac_plugin ++ str ":" ++ str ml.mltac_tactic ++ str ">" + str "Prim <" ++ str ml.mltac_plugin ++ str ":" ++ str ml.mltac_tactic ++ str ">" | FrExtn (tag, arg) -> let obj = Tac2env.interp_ml_object tag in - obj.Tac2env.ml_print (Global.env ()) arg + str "Extn " ++ str (Tac2dyn.Arg.repr tag) ++ str ":" ++ spc () ++ + obj.Tac2env.ml_print (Global.env ()) arg let () = register_handler begin function | Tac2interp.LtacError (kn, _, bt) -> |