diff options
| author | Pierre-Marie Pédrot | 2017-09-07 16:06:04 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-07 16:27:06 +0200 |
| commit | d577fe086794fda2edb3b98c12606e24c9c92ea1 (patch) | |
| tree | 0be06255fc7f48a8eea204f2d96f4b94a1e1acb8 /src | |
| parent | 2bea4137bd0841de7273a5adf9a72bd2e786fb68 (diff) | |
Fix coq/ltac2#21: Backtraces should print Ltac2 closures.
Diffstat (limited to 'src')
| -rw-r--r-- | src/tac2entries.ml | 4 | ||||
| -rw-r--r-- | src/tac2expr.mli | 3 | ||||
| -rw-r--r-- | src/tac2interp.ml | 8 |
3 files changed, 10 insertions, 5 deletions
diff --git a/src/tac2entries.ml b/src/tac2entries.ml index eed7eb6def..d596a61152 100644 --- a/src/tac2entries.ml +++ b/src/tac2entries.ml @@ -757,8 +757,8 @@ let _ = Goptions.declare_bool_option { } let pr_frame = function -| FrLtac None -> str "Call <anonymous>" -| FrLtac (Some kn) -> +| FrAnon e -> str "Call <anonymous:" ++ pr_glbexpr e ++ str ">" +| FrLtac kn -> str "Call " ++ Libnames.pr_qualid (Tac2env.shortest_qualid_of_ltac (TacConstant kn)) | FrPrim ml -> str "Prim <" ++ str ml.mltac_plugin ++ str ":" ++ str ml.mltac_tactic ++ str ">" diff --git a/src/tac2expr.mli b/src/tac2expr.mli index 77e2cfef0e..0b9923f7b9 100644 --- a/src/tac2expr.mli +++ b/src/tac2expr.mli @@ -181,7 +181,8 @@ type strexpr = type tag = int type frame = -| FrLtac of ltac_constant option +| FrLtac of ltac_constant +| FrAnon of glb_tacexpr | FrPrim of ml_tactic_name | FrExtn : ('a, 'b) Tac2dyn.Arg.tag * 'b -> frame diff --git a/src/tac2interp.ml b/src/tac2interp.ml index f37b4f8e9c..19efeb7669 100644 --- a/src/tac2interp.ml +++ b/src/tac2interp.ml @@ -140,10 +140,14 @@ let rec interp (ist : environment) = function and interp_app f = (); fun args -> match f with | { clos_env = ist; clos_var = ids; clos_exp = e; clos_ref = kn } -> + let frame = match kn with + | None -> FrAnon e + | Some kn -> FrLtac kn + in let rec push ist ids args = match ids, args with - | [], [] -> with_frame (FrLtac kn) (interp ist e) + | [], [] -> with_frame frame (interp ist e) | [], _ :: _ -> - with_frame (FrLtac kn) (interp ist e) >>= fun f -> Tac2ffi.to_closure f args + with_frame frame (interp ist e) >>= fun f -> Tac2ffi.to_closure f args | _ :: _, [] -> let cls = { clos_ref = kn; clos_env = ist.env_ist; clos_var = ids; clos_exp = e } in let f = interp_app cls in |