Skip to content
Snippets Groups Projects
Commit 348ddc06 authored by Ralf Jung's avatar Ralf Jung
Browse files

fix build

parent 9b7f6a5c
No related branches found
No related tags found
No related merge requests found
Pipeline #
Hide whitespace changes
Inline Side-by-side
theories/typing/function.v
+ 2
− 2
View file @ 348ddc06
...@@ -109,7 +109,7 @@ Section typing. ...@@ -109,7 +109,7 @@ Section typing.
(∀ x, subtype (E0 ++ E x) L0 (ty1 x) (ty2 x)) → (∀ x, subtype (E0 ++ E x) L0 (ty1 x) (ty2 x)) →
subtype E0 L0 (fn E tys1 ty1) (fn E tys2 ty2). subtype E0 L0 (fn E tys1 ty1) (fn E tys2 ty2).
Proof. Proof.
intros. apply fn_subtype_full; try done. intros. apply elctx_incl_refl. intros. apply fn_subtype_full; try done.
Qed. Qed.
(* This proper and the next can probably not be inferred, but oh well. *) (* This proper and the next can probably not be inferred, but oh well. *)
...@@ -145,7 +145,7 @@ Section typing. ...@@ -145,7 +145,7 @@ Section typing.
intros Hκκ'. apply fn_subtype_full; try done. intros. intros Hκκ'. apply fn_subtype_full; try done. intros.
apply elctx_incl_lft_incl; last by apply elctx_incl_refl. apply elctx_incl_lft_incl; last by apply elctx_incl_refl.
iIntros "#HE #HL". iApply (Hκκ' with "[HE] HL"). iIntros "#HE #HL". iApply (Hκκ' with "[HE] HL").
rewrite /elctx_interp_0 big_sepL_app. iDestruct "HE" as "[_ $]". rewrite /elctx_interp_0 big_sepL_app. iDestruct "HE" as "[$ _]".
Qed. Qed.
Lemma fn_subtype_specialize {A B n} (σ : A → B) E0 L0 E tys ty : Lemma fn_subtype_specialize {A B n} (σ : A → B) E0 L0 E tys ty :
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment