From b81d90d82c7da531022c37338ef8484b261e9a1b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maxime=20D=C3=A9n=C3=A8s?= <maxime.denes@inria.fr>
Date: Fri, 1 Feb 2019 14:15:28 +0100
Subject: [PATCH] Remove `Local` attribute for `Inductive`

This was a noop and will soon be an error (until `Inductive` properly
supports locality attributes). See https://github.com/coq/coq/pull/9410
---
 theories/proofmode/ltac_tactics.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 21556d314..cf2661ddd 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -143,7 +143,7 @@ Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
      let H2 := pretty_ident H2 in
      fail "iRename:" H2 "not fresh"|].
 
-Local Inductive esel_pat :=
+Inductive esel_pat :=
   | ESelPure
   | ESelIdent : bool → ident → esel_pat.
 
-- 
GitLab