Quick-and-dirty backtrace mechanism for the interpreter.

1 files changed, 12 insertions, 2 deletions

diff --git a/src/tac2expr.mli b/src/tac2expr.mli
index 470323e7c7..36c3fbbe59 100644
--- a/src/tac2expr.mli
+++ b/src/tac2expr.mli
@@ -205,6 +205,16 @@ and closure = {
   (** Global constant from which the closure originates *)
 }
 
-type ml_tactic = valexpr list -> valexpr Proofview.tactic
+type frame =
+| FrLtac of ltac_constant option
+| FrPrim of ml_tactic_name
+| FrExtn : ('a, 'b) Tac2dyn.Arg.tag * 'b -> frame
 
-type environment = valexpr Id.Map.t
+type backtrace = frame list
+
+type ml_tactic = backtrace -> valexpr list -> valexpr Proofview.tactic
+
+type environment = {
+  env_ist : valexpr Id.Map.t;
+  env_bkt : backtrace;
+}