aboutsummaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
authorEnrico Tassi2020-11-23 16:47:06 +0100
committerEnrico Tassi2020-11-23 16:47:06 +0100
commit17da7c41b17da3280cb2c182387685ad4be6022f (patch)
treee96191ea4e4bc5650154bacb0f027d586355f541 /toplevel
parentd41bb0c5e15442da6f6b7333e2b1e73a8091292a (diff)
Update compat infrastructure for 8.14
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/coqargs.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index ec339c69c6..fbf3b4873b 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -261,6 +261,7 @@ let get_native_name s =
with _ -> ""
let get_compat_file = function
+ | "8.14" -> "Coq.Compat.Coq814"
| "8.13" -> "Coq.Compat.Coq813"
| "8.12" -> "Coq.Compat.Coq812"
| "8.11" -> "Coq.Compat.Coq811"