From 409bc943e8d8a0bc0d35ae63f3530b7324ca975e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 17 Oct 2016 17:24:32 +0200
Subject: Fix previous commit.

I've messed up with parts of the compatibility files I had to commit.
---
 theories/Compat/Coq85.v | 18 ------------------
 1 file changed, 18 deletions(-)

diff --git a/theories/Compat/Coq85.v b/theories/Compat/Coq85.v
index 74b416aae7..4007536442 100644
--- a/theories/Compat/Coq85.v
+++ b/theories/Compat/Coq85.v
@@ -27,21 +27,3 @@ Global Set Refolding Reduction.
 Global Set Typeclasses Legacy Resolution.
 Global Set Typeclasses Limit Intros.
 Global Unset Typeclasses Filtered Unification.
-
-(** In Coq 8.5, [] meant Vector, and [ ] meant list.  Restore this
-    behavior, to allow user-defined [] to not override vector
-    notations.  See https://coq.inria.fr/bugs/show_bug.cgi?id=4785. *)
-
-Require Coq.Lists.List.
-Require Coq.Vectors.VectorDef.
-Module Export Coq.
-Module Export Vectors.
-Module VectorDef.
-Export Coq.Vectors.VectorDef.
-Module VectorNotations.
-Export Coq.Vectors.VectorDef.VectorNotations.
-Notation "[]" := (VectorDef.nil _) : vector_scope.
-End VectorNotations.
-End VectorDef.
-End Vectors.
-End Coq.
-- 
cgit v1.2.3