From d2b017680cb556160be604136be74d23a7237d68 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 9 Jan 2017 09:04:07 +0100
Subject: [PATCH] Make the pattern for [tctx_extract_hasty_here_eq] more
 robust.

---
 theories/typing/type_context.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 4e286659..d9844bd9 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -363,5 +363,5 @@ Hint Resolve tctx_extract_blocked_here tctx_extract_blocked_cons
    the environment if the type is copy. But due to a bug in Coq, we
    cannot enforce this using [Hint Resolve]. Cf:
        https://coq.inria.fr/bugs/show_bug.cgi?id=5299 *)
-Hint Extern 2 (tctx_extract_hasty _ _ ?p _ ((?p ◁ _) :: _) _) =>
+Hint Extern 2 (tctx_extract_hasty _ _ _ _ ((_ ◁ _) :: _) _) =>
   eapply tctx_extract_hasty_here_eq.
-- 
GitLab