From 3ff124b7a655ad49b642b7ba0dfdd8884b8aefa1 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jjourdan@mpi-sws.org>
Date: Thu, 5 Jan 2017 15:04:43 +0100
Subject: [PATCH] Fix build.
---
theories/typing/function.v | 2 +-
theories/typing/lft_contexts.v | 4 ++--
2 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/theories/typing/function.v b/theories/typing/function.v
index c649ca84..59ab07fe 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -209,7 +209,7 @@ Section typing.
intros Hfn HE HTT' HC HT'T''.
rewrite -typed_body_mono /flip; last done; first by eapply type_call.
- etrans. eapply (incl_cctx_incl _ [_]); first by intros ? ->%elem_of_list_singleton.
- apply cctx_incl_cons; first done. intros args. inv_vec args=>ret q. inv_vec q. done.
+ apply cctx_incl_cons_match; first done. intros args. inv_vec args=>ret q. inv_vec q. done.
- etrans; last by apply (tctx_incl_frame_l _ _ [_]).
apply copy_elem_of_tctx_incl; last done. apply _.
Qed.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 486b54bf..0ec04a9c 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -436,9 +436,9 @@ Hint Resolve
(* We declare these as hint extern, so that the [B] parameter of elem_of does
not have to be [list _] and can be an alias of this. *)
Hint Extern 0 (@elem_of _ _ (@elem_of_list _) _ (_ :: _)) =>
- eapply @elem_of_list_here.
+ eapply @elem_of_list_here : lrust_typing.
Hint Extern 1 (@elem_of _ _ (@elem_of_list _) _ (_ :: _)) =>
- eapply @elem_of_list_further.
+ eapply @elem_of_list_further : lrust_typing.
Hint Resolve lctx_lft_alive_external' | 100 : lrust_typing.
--
GitLab