From 3ce123f16ce19f67dde4a0f3f2874a2678649907 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
Date: Tue, 20 Feb 2018 16:03:57 +0100
Subject: Remove 8.5 compatibility support.

---
 theories/Compat/Coq85.v | 36 ------------------------------------
 1 file changed, 36 deletions(-)
 delete mode 100644 theories/Compat/Coq85.v

(limited to 'theories')

diff --git a/theories/Compat/Coq85.v b/theories/Compat/Coq85.v
deleted file mode 100644
index 56a9130d1..000000000
--- a/theories/Compat/Coq85.v
+++ /dev/null
@@ -1,36 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** Compatibility file for making Coq act similar to Coq v8.5 *)
-
-(** Any compatibility changes to make future versions of Coq behave like Coq 8.6
-    are likely needed to make them behave like Coq 8.5. *)
-Require Export Coq.Compat.Coq86.
-
-(** We use some deprecated options in this file, so we disable the
-    corresponding warning, to silence the build of this file. *)
-Local Set Warnings "-deprecated-option".
-
-(* In 8.5, "intros [|]", taken e.g. on a goal "A\/B->C", does not
-   behave as "intros [H|H]" but leave instead hypotheses quantified in
-   the goal, here producing subgoals A->C and B->C. *)
-
-Global Unset Bracketing Last Introduction Pattern.
-Global Unset Regular Subst Tactic.
-Global Unset Structural Injection.
-Global Unset Shrink Abstract.
-Global Unset Shrink Obligations.
-Global Set Refolding Reduction.
-
-(** The resolution algorithm for type classes has changed. *)
-Global Set Typeclasses Legacy Resolution.
-Global Set Typeclasses Limit Intros.
-Global Unset Typeclasses Filtered Unification.
-
-(** Allow silently letting unification constraints float after a "." *)
-Global Unset Solve Unification Constraints.
-- 
cgit v1.2.3