From db57a33e3d377c7aced21fdaf60debb022d4e219 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 15 Jun 2018 22:47:26 +0200
Subject: [PATCH] Make Ltac helper function local

---
 tests/proofmode.ref               | 4 ++--
 theories/proofmode/ltac_tactics.v | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 0946b2643..aa47143c6 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -36,11 +36,11 @@ Ltac call to "done" failed.
 No applicable tactic.
 The command has indeed failed with message:
 In nested Ltac calls to "iClear (constr)", "iElaborateSelPat" and
-"iElaborateSelPat_go", last call failed.
+"<iris.proofmode.ltac_tactics.iElaborateSelPat_go>", last call failed.
 Tactic failure: iElaborateSelPat: "HQ" not found.
 The command has indeed failed with message:
 In nested Ltac calls to "iClear (constr)", "iElaborateSelPat" and
-"iElaborateSelPat_go", last call failed.
+"<iris.proofmode.ltac_tactics.iElaborateSelPat_go>", last call failed.
 Tactic failure: iElaborateSelPat: "HQ" not found.
 The command has indeed failed with message:
 In nested Ltac calls to "iSpecialize (open_constr)",
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 094d74b2d..4d5015b3c 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -140,7 +140,7 @@ Local Inductive esel_pat :=
   | ESelPure
   | ESelIdent : bool → ident → esel_pat.
 
-Ltac iElaborateSelPat_go pat Δ Hs :=
+Local Ltac iElaborateSelPat_go pat Δ Hs :=
   lazymatch pat with
   | [] => eval cbv in Hs
   | SelPure :: ?pat =>  iElaborateSelPat_go pat Δ (ESelPure :: Hs)
-- 
GitLab