aboutsummaryrefslogtreecommitdiffstats
path: root/backend/CMparser.mly
diff options
context:
space:
mode:
Diffstat (limited to 'backend/CMparser.mly')
-rw-r--r--backend/CMparser.mly2
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/CMparser.mly b/backend/CMparser.mly
index 94b50810..64943f0b 100644
--- a/backend/CMparser.mly
+++ b/backend/CMparser.mly
@@ -17,7 +17,7 @@
including function calls in expressions, matches, while statements, etc. */
%{
-open !Datatypes
+open Datatypes
open Camlcoq
open BinNums
open Integers