From c6c5de4767fc4592e92413b5f304537dc8b53287 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 19 May 2019 17:38:01 +0200
Subject: [PATCH] Try to fix compilation with Coq 8.7.*.

---
 theories/proofmode/ltac_tactics.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 550db0c5e..f831bb819 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -101,7 +101,7 @@ Ltac iFresh :=
   side-effect (i.e. to bump the counter) and to return a value (the fresh name).
   We do this by wrapped the side-effect under a [match] in a let-binding. See
   https://stackoverflow.com/a/46178884 *)
-  let _ :=
+  let start :=
     lazymatch goal with
     | _ => iStartProof
     end in
@@ -109,7 +109,7 @@ Ltac iFresh :=
     lazymatch goal with
     | |- envs_entails (Envs _ _ ?c) _ => c
     end in
-  let _ :=
+  let inc :=
     lazymatch goal with
     | |- envs_entails (Envs ?Δp ?Δs _) ?Q =>
       let c' := eval vm_compute in (Pos.succ c) in
-- 
GitLab