From 4a412dae5f01d669eda2a04a101510a6516b44a2 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Sat, 23 Nov 2024 11:31:13 -0800
Subject: [PATCH] change mcltt to mctt

---
 theories/Core/Completeness/EqualityCases.v    | 16 ++---
 theories/Core/Semantic/PER/Definitions.v      |  4 +-
 theories/Core/Semantic/PER/Lemmas.v           |  4 +-
 .../Soundness/LogicalRelation/CoreLemmas.v    |  6 +-
 theories/Core/Syntactic/Presup.v              | 58 +++++++++----------
 5 files changed, 44 insertions(+), 44 deletions(-)

diff --git a/theories/Core/Completeness/EqualityCases.v b/theories/Core/Completeness/EqualityCases.v
index 946bda5..74243e7 100644
--- a/theories/Core/Completeness/EqualityCases.v
+++ b/theories/Core/Completeness/EqualityCases.v
@@ -30,7 +30,7 @@ Proof.
   per_univ_elem_econstructor; mauto 3; try solve_refl.
 Qed.
 #[export]
-Hint Resolve rel_exp_eq_cong : mcltt.
+Hint Resolve rel_exp_eq_cong : mctt.
 
 Lemma valid_exp_eq : forall {Γ i A M1 M2},
     {{ Γ ⊨ A : Type@i }} ->
@@ -40,7 +40,7 @@ Lemma valid_exp_eq : forall {Γ i A M1 M2},
 Proof. mauto. Qed.
 
 #[export]
-Hint Resolve valid_exp_eq : mcltt.
+Hint Resolve valid_exp_eq : mctt.
 
 Lemma rel_exp_refl_cong : forall {Γ i A A' M M'},
     {{ Γ ⊨ A ≈ A' : Type@i }} ->
@@ -67,7 +67,7 @@ Proof.
     symmetry; mauto 3.
 Qed.
 #[export]
-Hint Resolve rel_exp_refl_cong : mcltt.
+Hint Resolve rel_exp_refl_cong : mctt.
 
 Lemma rel_exp_eq_sub : forall {Γ σ Δ i A M1 M2},
     {{ Γ ⊨s σ : Δ }} ->
@@ -97,7 +97,7 @@ Proof.
 Qed.
 
 #[export]
-Hint Resolve rel_exp_eq_sub : mcltt.
+Hint Resolve rel_exp_eq_sub : mctt.
 
 Lemma rel_exp_refl_sub : forall {Γ σ Δ i A M},
     {{ Γ ⊨s σ : Δ }} ->
@@ -126,7 +126,7 @@ Proof.
 Qed.
 
 #[export]
-Hint Resolve rel_exp_refl_sub : mcltt.
+Hint Resolve rel_exp_refl_sub : mctt.
 
 Lemma rel_exp_eqrec_sub : forall {Γ σ Δ i A M1 M2 j B BR N},
     {{ Γ ⊨s σ : Δ }} ->
@@ -208,7 +208,7 @@ Proof.
     It might be better to do some optimization first. *)
 Admitted.
 #[export]
-Hint Resolve rel_exp_eqrec_sub : mcltt.
+Hint Resolve rel_exp_eqrec_sub : mctt.
 
 Lemma rel_exp_eqrec_cong : forall {Γ i A A' M1 M1' M2 M2' j B B' BR BR' N N'},
     {{ Γ ⊨ A : Type@i }} ->
@@ -226,7 +226,7 @@ Lemma rel_exp_eqrec_cong : forall {Γ i A A' M1 M1' M2 M2' j B B' BR BR' N N'},
 Proof.
 Admitted.
 #[export]
-Hint Resolve rel_exp_eqrec_cong : mcltt.
+Hint Resolve rel_exp_eqrec_cong : mctt.
 
 Lemma rel_exp_eqrec_beta : forall {Γ i A M j B BR},
     {{ Γ ⊨ A : Type@i }} ->
@@ -239,4 +239,4 @@ Lemma rel_exp_eqrec_beta : forall {Γ i A M j B BR},
 Proof.
 Admitted.
 #[export]
-Hint Resolve rel_exp_eqrec_beta : mcltt.
+Hint Resolve rel_exp_eqrec_beta : mctt.
diff --git a/theories/Core/Semantic/PER/Definitions.v b/theories/Core/Semantic/PER/Definitions.v
index a1e6d2d..bfae7a2 100644
--- a/theories/Core/Semantic/PER/Definitions.v
+++ b/theories/Core/Semantic/PER/Definitions.v
@@ -82,7 +82,7 @@ Variant per_eq (point_rel : relation domain) m1 m2' : relation domain :=
      {{ Dom ⇑ a n ≈ ⇑ a' n' ∈ per_eq point_rel m1 m2' }} }
 .
 #[export]
-Hint Constructors per_eq : mcltt.
+Hint Constructors per_eq : mctt.
 
 Variant per_ne : relation domain :=
 | per_ne_neut :
@@ -319,7 +319,7 @@ Variant cons_per_ctx_env tail_rel (head_rel : forall {ρ ρ'} (equiv_ρ_ρ' : {{
         {{ Dom ^(ρ 0) ≈ ^(ρ' 0) ∈ head_rel equiv_ρ_drop_ρ'_drop }} ->
         {{ Dom ρ ≈ ρ' ∈ cons_per_ctx_env tail_rel (@head_rel) }} }.
 #[export]
-Hint Constructors cons_per_ctx_env : mcltt.
+Hint Constructors cons_per_ctx_env : mctt.
 
 Inductive per_ctx_env : relation env -> ctx -> ctx -> Prop :=
 | per_ctx_env_nil :
diff --git a/theories/Core/Semantic/PER/Lemmas.v b/theories/Core/Semantic/PER/Lemmas.v
index 3477df6..bf198d1 100644
--- a/theories/Core/Semantic/PER/Lemmas.v
+++ b/theories/Core/Semantic/PER/Lemmas.v
@@ -184,7 +184,7 @@ Proof with mautosolve 3.
 Qed.
 
 #[export]
-Hint Resolve per_eq_sym : mcltt.
+Hint Resolve per_eq_sym : mctt.
 
 Lemma per_eq_trans : forall point_rel m1 m2 n n' n'',
     PER point_rel ->
@@ -198,7 +198,7 @@ Proof with mautosolve 3.
 Qed.
 
 #[export]
-Hint Resolve per_eq_trans : mcltt.
+Hint Resolve per_eq_trans : mctt.
 
 #[export]
 Instance per_eq_PER {point_rel m1 m2} {Hpoint : PER point_rel} : PER (per_eq point_rel m1 m2).
diff --git a/theories/Core/Soundness/LogicalRelation/CoreLemmas.v b/theories/Core/Soundness/LogicalRelation/CoreLemmas.v
index 8150c44..0af7310 100644
--- a/theories/Core/Soundness/LogicalRelation/CoreLemmas.v
+++ b/theories/Core/Soundness/LogicalRelation/CoreLemmas.v
@@ -679,7 +679,7 @@ Proof.
 Qed.
 
 #[local]
- Hint Resolve glu_nat_resp_per_nat : mcltt.
+ Hint Resolve glu_nat_resp_per_nat : mctt.
 
 #[local]
   Ltac resp_per_IH :=
@@ -965,7 +965,7 @@ Proof.
       destruct_rel_mod_eval.
       simplify_evals.
       deepexec H1 ltac:(fun H => pose proof H).
-      autorewrite with mcltt in *.
+      autorewrite with mctt in *.
       mauto 3.
 
   - simpl_glu_rel.
@@ -1043,7 +1043,7 @@ Proof.
     split; [mauto 3 |].
     intros.
     saturate_weakening_escape.
-    autorewrite with mcltt.
+    autorewrite with mctt.
     mauto 3.
   - simpl_glu_rel.
     econstructor; repeat split; mauto 3;
diff --git a/theories/Core/Syntactic/Presup.v b/theories/Core/Syntactic/Presup.v
index e4ecaf7..d2c8d5e 100644
--- a/theories/Core/Syntactic/Presup.v
+++ b/theories/Core/Syntactic/Presup.v
@@ -33,7 +33,7 @@ Proof.
 Qed.
 
 #[local]
-Hint Resolve presup_exp_eq_natrec_cong_right : mcltt.
+Hint Resolve presup_exp_eq_natrec_cong_right : mctt.
 
 Lemma presup_exp_eq_natrec_sub_left : forall {Γ σ Δ i A MZ MS M},
     {{ ⊢ Γ }} ->
@@ -58,7 +58,7 @@ Proof.
 Qed.
 
 #[local]
-Hint Resolve presup_exp_eq_natrec_sub_left : mcltt.
+Hint Resolve presup_exp_eq_natrec_sub_left : mctt.
 
 Lemma presup_exp_eq_natrec_sub_right : forall {Γ σ Δ i A MZ MS M},
     {{ ⊢ Γ }} ->
@@ -112,7 +112,7 @@ Proof.
 Qed.
 
 #[local]
-Hint Resolve presup_exp_eq_natrec_sub_right : mcltt.
+Hint Resolve presup_exp_eq_natrec_sub_right : mctt.
 
 Lemma presup_exp_eq_beta_succ_right : forall {Γ i A MZ MS M},
     {{ ⊢ Γ, ℕ }} ->
@@ -156,7 +156,7 @@ Proof.
 Qed.
 
 #[local]
-Hint Resolve presup_exp_eq_beta_succ_right : mcltt.
+Hint Resolve presup_exp_eq_beta_succ_right : mctt.
 
 Lemma presup_exp_eq_fn_cong_right : forall {Γ i A A' j B M'},
     {{ ⊢ Γ }} ->
@@ -179,7 +179,7 @@ Proof.
 Qed.
 
 #[local]
-Hint Resolve presup_exp_eq_fn_cong_right : mcltt.
+Hint Resolve presup_exp_eq_fn_cong_right : mctt.
 
 Lemma presup_exp_eq_fn_sub_right : forall {Γ σ Δ i A j B M},
     {{ ⊢ Γ }} ->
@@ -204,7 +204,7 @@ Proof.
 Qed.
 
 #[local]
-Hint Resolve presup_exp_eq_fn_sub_right : mcltt.
+Hint Resolve presup_exp_eq_fn_sub_right : mctt.
 
 Lemma presup_exp_eq_app_cong_right : forall {Γ i A B M' N N'},
     {{ ⊢ Γ }} ->
@@ -227,7 +227,7 @@ Proof.
 Qed.
 
 #[local]
-Hint Resolve presup_exp_eq_app_cong_right : mcltt.
+Hint Resolve presup_exp_eq_app_cong_right : mctt.
 
 Lemma presup_exp_eq_app_sub_left : forall {Γ σ Δ i A B M N},
     {{ ⊢ Γ }} ->
@@ -258,7 +258,7 @@ Proof.
 Qed.
 
 #[local]
-Hint Resolve presup_exp_eq_app_sub_left : mcltt.
+Hint Resolve presup_exp_eq_app_sub_left : mctt.
 
 Lemma presup_exp_eq_app_sub_right : forall {Γ σ Δ i A B M N},
     {{ ⊢ Γ }} ->
@@ -287,7 +287,7 @@ Proof.
 Qed.
 
 #[local]
-Hint Resolve presup_exp_eq_app_sub_right : mcltt.
+Hint Resolve presup_exp_eq_app_sub_right : mctt.
 
 Lemma presup_exp_eq_pi_eta_right : forall {Γ i A B M},
     {{ ⊢ Γ }} ->
@@ -312,7 +312,7 @@ Proof.
 Qed.
 
 #[local]
-Hint Resolve presup_exp_eq_pi_eta_right : mcltt.
+Hint Resolve presup_exp_eq_pi_eta_right : mctt.
 
 Lemma presup_exp_eq_prop_eq_var0 : forall {Γ i A},
     {{ Γ ⊢ A : Type@i }} ->
@@ -326,7 +326,7 @@ Proof.
 Qed.
 
 #[export]
-Hint Resolve presup_exp_eq_prop_eq_var0 : mcltt.
+Hint Resolve presup_exp_eq_prop_eq_var0 : mctt.
 
 Lemma presup_exp_eq_prop_eq_var1 : forall {Γ i A},
     {{ Γ ⊢ A : Type@i }} ->
@@ -340,7 +340,7 @@ Proof.
 Qed.
 
 #[export]
-Hint Resolve presup_exp_eq_prop_eq_var1 : mcltt.
+Hint Resolve presup_exp_eq_prop_eq_var1 : mctt.
 
 Lemma presup_exp_eq_prop_eq_wf : forall {Γ i A},
     {{ Γ ⊢ A : Type@i }} ->
@@ -356,7 +356,7 @@ Proof.
 Qed.
 
 #[export]
-Hint Resolve presup_exp_eq_prop_eq_wf : mcltt.
+Hint Resolve presup_exp_eq_prop_eq_wf : mctt.
 
 Lemma presup_exp_eq_prop_eq_sub_helper2 : forall {Γ σ Δ i A M1 M2},
     {{ Γ ⊢s σ : Δ }} ->
@@ -377,7 +377,7 @@ Proof.
 Qed.
 
 #[export]
-Hint Resolve presup_exp_eq_prop_eq_sub_helper2 : mcltt.
+Hint Resolve presup_exp_eq_prop_eq_sub_helper2 : mctt.
 
 Lemma presup_exp_eq_prop_eq_typ_sub2_eq : forall {Γ σ Δ i A M1 M2},
     {{ Γ ⊢s σ : Δ }} ->
@@ -407,7 +407,7 @@ Proof.
 Qed.
 
 #[export]
-Hint Resolve presup_exp_eq_prop_eq_typ_sub2_eq : mcltt.
+Hint Resolve presup_exp_eq_prop_eq_typ_sub2_eq : mctt.
 
 Lemma presup_exp_eq_prop_eq_sub_helper3 : forall {Γ σ Δ i A M1 M2 N},
     {{ Γ ⊢s σ : Δ }} ->
@@ -426,7 +426,7 @@ Proof.
 Qed.
 
 #[export]
-Hint Resolve presup_exp_eq_prop_eq_sub_helper3 : mcltt.
+Hint Resolve presup_exp_eq_prop_eq_sub_helper3 : mctt.
 
 Lemma presup_exp_eq_prop_eq_id_sub_helper2 : forall {Γ i A M1 M2},
     {{ Γ ⊢ A : Type@i }} ->
@@ -447,7 +447,7 @@ Proof.
 Qed.
 
 #[export]
-Hint Resolve presup_exp_eq_prop_eq_id_sub_helper2 : mcltt.
+Hint Resolve presup_exp_eq_prop_eq_id_sub_helper2 : mctt.
 
 Lemma presup_exp_eq_prop_eq_typ_id_sub2_eq : forall {Γ i A M1 M2},
     {{ Γ ⊢ A : Type@i }} ->
@@ -472,7 +472,7 @@ Proof.
 Qed.
 
 #[export]
-Hint Resolve presup_exp_eq_prop_eq_typ_id_sub2_eq : mcltt.
+Hint Resolve presup_exp_eq_prop_eq_typ_id_sub2_eq : mctt.
 
 Lemma presup_exp_eq_prop_eq_id_sub_helper3 : forall {Γ i A M1 M2 N},
     {{ Γ ⊢ A : Type@i }} ->
@@ -490,7 +490,7 @@ Proof.
 Qed.
 
 #[export]
-Hint Resolve presup_exp_eq_prop_eq_id_sub_helper3 : mcltt.
+Hint Resolve presup_exp_eq_prop_eq_id_sub_helper3 : mctt.
 
 Lemma presup_exp_eq_refl_sub_right : forall {Γ σ Δ i A M},
     {{ ⊢ Γ }} ->
@@ -509,7 +509,7 @@ Proof.
 Qed.
 
 #[local]
-Hint Resolve presup_exp_eq_refl_sub_right : mcltt.
+Hint Resolve presup_exp_eq_refl_sub_right : mctt.
 
 Lemma presup_exp_eq_eqrec_sub_left : forall {Γ σ Δ i A M1 M2 j B N BR},
     {{ ⊢ Γ }} ->
@@ -554,7 +554,7 @@ Proof.
 Qed.
 
 #[local]
-Hint Resolve presup_exp_eq_eqrec_sub_left : mcltt.
+Hint Resolve presup_exp_eq_eqrec_sub_left : mctt.
 
 Lemma presup_exp_eq_eqrec_sub_right : forall {Γ σ Δ i A M1 M2 j B N BR},
     {{ ⊢ Γ }} ->
@@ -881,7 +881,7 @@ Proof.
 Qed.
 
 #[local]
-Hint Resolve presup_exp_eq_eqrec_sub_right : mcltt.
+Hint Resolve presup_exp_eq_eqrec_sub_right : mctt.
 
 Lemma presup_exp_eq_refl_cong_right : forall {Γ i A A' M M'},
     {{ ⊢ Γ }} ->
@@ -899,7 +899,7 @@ Proof.
 Qed.
 
 #[local]
-Hint Resolve presup_exp_eq_refl_cong_right : mcltt.
+Hint Resolve presup_exp_eq_refl_cong_right : mctt.
 
 Lemma presup_exp_eq_eqrec_cong_right : forall {Γ i A A' M1 M1' M2 M2' j B B' BR BR' N N'},
     {{ ⊢ Γ }} ->
@@ -1029,7 +1029,7 @@ Proof.
 Qed.
 
 #[local]
-Hint Resolve presup_exp_eq_eqrec_cong_right : mcltt.
+Hint Resolve presup_exp_eq_eqrec_cong_right : mctt.
 
 Lemma presup_exp_eq_eqrec_beta_right : forall {Γ i A M j B BR},
     {{ ⊢ Γ }} ->
@@ -1137,7 +1137,7 @@ Proof.
 Qed.
 
 #[local]
-Hint Resolve presup_exp_eq_eqrec_beta_right : mcltt.
+Hint Resolve presup_exp_eq_eqrec_beta_right : mctt.
 
 Lemma presup_exp_eq_var_0_sub_left : forall {Γ σ Δ i A M},
     {{ ⊢ Γ }} ->
@@ -1154,7 +1154,7 @@ Proof.
 Qed.
 
 #[local]
-Hint Resolve presup_exp_eq_var_0_sub_left : mcltt.
+Hint Resolve presup_exp_eq_var_0_sub_left : mctt.
 
 Lemma presup_exp_eq_var_S_sub_left : forall {Γ σ Δ i A M B x},
     {{ ⊢ Γ }} ->
@@ -1173,7 +1173,7 @@ Proof.
 Qed.
 
 #[local]
-Hint Resolve presup_exp_eq_var_S_sub_left : mcltt.
+Hint Resolve presup_exp_eq_var_S_sub_left : mctt.
 
 Lemma presup_exp_eq_sub_cong_right : forall {Γ σ σ' Δ i A M M'},
     {{ ⊢ Δ }} ->
@@ -1193,7 +1193,7 @@ Proof.
 Qed.
 
 #[local]
-Hint Resolve presup_exp_eq_sub_cong_right : mcltt.
+Hint Resolve presup_exp_eq_sub_cong_right : mctt.
 
 Lemma presup_exp_eq_sub_compose_right : forall {Γ τ Γ' σ Γ'' i A M},
     {{ ⊢ Γ }} ->
@@ -1210,7 +1210,7 @@ Proof.
 Qed.
 
 #[local]
-Hint Resolve presup_exp_eq_sub_compose_right : mcltt.
+Hint Resolve presup_exp_eq_sub_compose_right : mctt.
 
 #[local]
 Ltac gen_presup_IH presup_exp_eq presup_sub_eq presup_subtyp H :=