Merge pull request #1076 from ppedrot/setoid-type-core-tc-opaque

Adapt w.r.t. coq/coq#18910.
MetaCoq · Apr 9, 2024 · 74918fc · 74918fc
2 parents 6ec591b + 2d9b6f0
commit 74918fc
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/pcuic/theories/PCUICConfluence.v b/pcuic/theories/PCUICConfluence.v
@@ -1398,7 +1398,7 @@ Proof.
   destruct (@red1_eq_context_upto_l Σ Σ' (fun pb => flip (cmp_universe pb)) (fun pb => flip (cmp_sort pb)) pb Γ Δ u v) as (v' & r & e); tas.
   - intro x. red. reflexivity.
   - intro x. red. reflexivity.
-  - eapply eq_context_upto_flip; [..|eassumption]; tc.
+  - eapply eq_context_upto_flip; [..|eassumption]; unfold flip; tc.
   - exists v'; split; tas.
     eapply eq_term_upto_univ_napp_flip; [..|eassumption]; tc.
 Qed.