aboutsummaryrefslogtreecommitdiff
path: root/src/tac2stdlib.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/tac2stdlib.ml')
-rw-r--r--src/tac2stdlib.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index 6512510f0a..6b3b997232 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -12,6 +12,7 @@ open Globnames
open Misctypes
open Genredexpr
open Tac2expr
+open Tac2ffi
open Proofview.Notations
module Value = Tac2ffi