From d577fe086794fda2edb3b98c12606e24c9c92ea1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 7 Sep 2017 16:06:04 +0200
Subject: Fix coq/ltac2#21: Backtraces should print Ltac2 closures.

---
 src/tac2expr.mli | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'src/tac2expr.mli')

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
 
-- 
cgit v1.2.3