summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2024-06-05 17:51:24 +0200
committerSon Ho2024-06-05 17:51:24 +0200
commite6d04cf1a73533ae80a68d9ef5f34a9e832e77a3 (patch)
treec86de4d3100dc4b61850a62c407fa71fc67b6d46
parentbf3f474ed65fd6ad7a7ca3d5851c990231a857e7 (diff)
Fix a minor issue
-rw-r--r--compiler/ExtractBase.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index bc56dd28..4aac270f 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -883,6 +883,7 @@ let keywords () =
"Declare";
"Definition";
"else";
+ "end";
"End";
"fun";
"Fixpoint";