From a013bcff87b20dedb739087d975c2be71356d51d Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 11 Apr 2018 18:15:44 +0200
Subject: [PATCH] This Coq bug is fixed.

---
 theories/typing/base.v | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/theories/typing/base.v b/theories/typing/base.v
index a987f68f..88b675f5 100644
--- a/theories/typing/base.v
+++ b/theories/typing/base.v
@@ -23,8 +23,4 @@ Hint Extern 1 (@eq nat _ (Z.to_nat _)) =>
 Hint Extern 1 (@eq nat (Z.to_nat _) _) =>
   (etrans; [exact: Nat2Z.id | reflexivity]) : lrust_typing.
 
-(* FIXME : I would prefer using a [Hint Resolve <-] for this, but
-   unfortunately, this is not preserved across modules. See:
-     https://coq.inria.fr/bugs/show_bug.cgi?id=5189
-   This should be fixed in the next version of Coq. *)
-Hint Extern 1 (_ âˆˆ _ ++ _) => apply <- @elem_of_app : lrust_typing.
+Hint Resolve <- elem_of_app : lrust_typing.
-- 
GitLab