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/tac2expr.mli | |
| parent | 2bea4137bd0841de7273a5adf9a72bd2e786fb68 (diff) | |
Fix coq/ltac2#21: Backtraces should print Ltac2 closures.
Diffstat (limited to 'src/tac2expr.mli')
| -rw-r--r-- | src/tac2expr.mli | 3 |
1 files changed, 2 insertions, 1 deletions
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 |