From 769b3f4f095db13c69194d02de61309879e15bc3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Thu, 17 Jul 2025 17:00:17 +0200
Subject: [PATCH] Remove useless `...`

---
 theory/ua_products.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theory/ua_products.v b/theory/ua_products.v
index a269f64a..20abb03b 100644
--- a/theory/ua_products.v
+++ b/theory/ua_products.v
@@ -154,7 +154,7 @@ Section varieties.
        (λ i, eval et (λ sort n, vars sort n i) t) (λ i, eval et (λ sort n, vars sort n i) t0).
      intro.
      apply H2. clear H2. simpl.
-     induction entailment_premises... simpl in *.
+     induction entailment_premises. simpl in *.
      intuition.
      simpl.
      rewrite <- (nqe_always (fst (projT2 a)) vars i).