From ac3a3e4d6e9b6c7eb084dcfcd2df3228c3386dd0 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Wed, 29 Apr 2020 16:54:51 +0200
Subject: [PATCH] Fix a warning

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

diff --git a/theories/typing/interp.v b/theories/typing/interp.v
index aa03ce9..2845ffc 100644
--- a/theories/typing/interp.v
+++ b/theories/typing/interp.v
@@ -39,7 +39,7 @@ Section semtypes.
     | TExists τ' => λne Δ, lrel_exists (λ τ, interp τ' (τ::Δ))
     | Tref τ => λne Δ, lrel_ref (interp τ Δ)
     end.
-  Solve Obligations with (intros I τ τ' n Δ Δ' HΔ' ??; solve_proper).
+  Solve Obligations with (intros I τ τ' n Δ Δ' HΔ' ??; try solve_proper).
   Next Obligation.
     intros I τ τ' n Δ Δ' HΔ' ??.
     apply lrel_rec_ne=> X /=.
-- 
GitLab