aboutsummaryrefslogtreecommitdiff
path: root/src/tac2interp.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2017-09-14 21:28:32 +0200
committerPierre-Marie Pédrot2017-09-14 21:34:21 +0200
commit97bcc97fab0e9c0967c7f723e24ba0f238bd94ff (patch)
tree16179b89485290454765a50856999a1c45c751f6 /src/tac2interp.ml
parent7cee394fc0c6a7a28def2222be0289d6083f47c2 (diff)
Moving valexpr definition to Tac2ffi.
Diffstat (limited to 'src/tac2interp.ml')
-rw-r--r--src/tac2interp.ml5
1 files changed, 5 insertions, 0 deletions
diff --git a/src/tac2interp.ml b/src/tac2interp.ml
index 815fdffe0f..58a3a9a4ec 100644
--- a/src/tac2interp.ml
+++ b/src/tac2interp.ml
@@ -13,6 +13,7 @@ open Genarg
open Names
open Proofview.Notations
open Tac2expr
+open Tac2ffi
exception LtacError = Tac2ffi.LtacError
@@ -42,6 +43,10 @@ let with_frame frame tac =
Proofview.tclUNIT ans
else tac
+type environment = Tac2env.environment = {
+ env_ist : valexpr Id.Map.t;
+}
+
let empty_environment = {
env_ist = Id.Map.empty;
}