From 17da7c41b17da3280cb2c182387685ad4be6022f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 23 Nov 2020 16:47:06 +0100 Subject: Update compat infrastructure for 8.14 --- theories/Compat/Coq813.v | 2 ++ theories/Compat/Coq814.v | 11 +++++++++++ 2 files changed, 13 insertions(+) create mode 100644 theories/Compat/Coq814.v (limited to 'theories') diff --git a/theories/Compat/Coq813.v b/theories/Compat/Coq813.v index 92544c6ed9..fe7431dcd3 100644 --- a/theories/Compat/Coq813.v +++ b/theories/Compat/Coq813.v @@ -9,3 +9,5 @@ (************************************************************************) (** Compatibility file for making Coq act similar to Coq v8.13 *) + +Require Export Coq.Compat.Coq814. diff --git a/theories/Compat/Coq814.v b/theories/Compat/Coq814.v new file mode 100644 index 0000000000..94948dd280 --- /dev/null +++ b/theories/Compat/Coq814.v @@ -0,0 +1,11 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(*