Skip to content

Commit

Permalink
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
revert
Browse files Browse the repository at this point in the history
HuStmpHrrr committed Dec 18, 2024
1 parent ce7f979 commit cf6ce42
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions theories/Core/Soundness/LogicalRelation/Lemmas.v
Original file line number Diff line number Diff line change
@@ -1227,7 +1227,7 @@ Proof.
eapply glu_univ_elem_exp_conv; revgoals; mauto 3.
Qed.

#[export]
#[global]
Ltac invert_glu_rel_exp H :=
(unshelve eapply (glu_rel_exp_clean_inversion2 _ _) in H; shelve_unifiable; [eassumption | eassumption |];
simpl in H)
@@ -1397,7 +1397,7 @@ Ltac saturate_syn_judge1 :=
assert {{ Γ ⊢s τ : Γ' }} by mauto; fail_if_dup
end.

#[export]
#[global]
Ltac saturate_syn_judge :=
repeat saturate_syn_judge1.

@@ -1409,6 +1409,6 @@ Ltac invert_sem_judge1 :=
invert_glu_rel_sub H
end.

#[export]
#[global]
Ltac invert_sem_judge :=
repeat invert_sem_judge1.

0 comments on commit cf6ce42

Please sign in to comment.