From e0fd7c668bc284924c63a1f0a0e36fb4856c49e1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 27 Oct 2017 16:04:00 +0200
Subject: Adding a command to evaluate Ltac2 expressions.

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

(limited to 'src/tac2expr.mli')

diff --git a/src/tac2expr.mli b/src/tac2expr.mli
index e57b0ba3ef..89152dffe7 100644
--- a/src/tac2expr.mli
+++ b/src/tac2expr.mli
@@ -168,6 +168,8 @@ type strexpr =
   (** Syntactic extensions *)
 | StrMut of qualid located * raw_tacexpr
   (** Redefinition of mutable globals *)
+| StrRun of raw_tacexpr
+  (** Toplevel evaluation of an expression *)
 
 (** {5 Dynamic semantics} *)
 
-- 
cgit v1.2.3