From 3208a68e2c1b5f29fe33b54a66a2c361d3bfc531 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 2 Oct 2018 14:45:00 -0400
Subject: Update the -compat flags

Mostly via `dev/tools/update-compat.py --cur-version=8.9`

We just remove test-suite/success/FunindExtraction_compat86.v because,
except for the `Extraction iszero.` line at the bottom, it is a
duplicate of `test-suite/success/Funind.v` (except with `-compat 8.6`).

We also manually update a number of test-suite files to pre-emptively
remove compatibility notations (which used to be compat 8.6, but are now
compat 8.7).
---
 doc/stdlib/index-list.html.template | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/stdlib')

diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 0fa42cadad..4cbf75b715 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -600,8 +600,8 @@ through the <tt>Require Import</tt> command.</p>
   </dt>
   <dd>
     theories/Compat/AdmitAxiom.v
-    theories/Compat/Coq86.v
     theories/Compat/Coq87.v
     theories/Compat/Coq88.v
+    theories/Compat/Coq89.v
   </dd>
 </dl>
-- 
cgit v1.2.3