actually compile

Beluga-lang · Dec 27, 2024 · 6050e5f · 6050e5f
1 parent 109da68
commit 6050e5f
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/theories/Core/Soundness/EqualityCases.v b/theories/Core/Soundness/EqualityCases.v
@@ -169,7 +169,7 @@ Proof.
   simpl in *.
 
   repeat invert_glu_rel1.
-  clear_dups.
+  handle_functional_glu_univ_elem.
   saturate_glu_typ_from_el.
   unify_glu_univ_lvl i.
 

diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v
@@ -1026,7 +1026,7 @@ Ltac basic_invert_glu_ctx_env H :=
    destruct H as [? [? []]])
   + dependent destruction H.
 
-Ltac invert_glu_ctx_env H := basic_glu_ctx_env H.
+Ltac invert_glu_ctx_env H := basic_invert_glu_ctx_env H.
 
 Lemma glu_ctx_env_subtyp_sub_if : forall Γ Γ' Sb Sb' Δ σ ρ,
     {{ ⊢ Γ ⊆ Γ' }} ->