From db8b426ec89dea4b1139504942c4ac1845840827 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 29 Mar 2025 08:53:34 +0100
Subject: [PATCH] Fix comment that is messed up.

---
 stdpp/list_relations.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/stdpp/list_relations.v b/stdpp/list_relations.v
index 8e9c9237..20e83140 100644
--- a/stdpp/list_relations.v
+++ b/stdpp/list_relations.v
@@ -65,9 +65,9 @@ Global Hint Extern 0 (_ ⊆+ _) => reflexivity : core.
 (** * Basic tactics on lists *)
 (** These are used already in this file so we cannot have them in [list_tactics]. *)
 
-(** The tactic [discriminate_list] discharges a goal if it submseteq
-a list equality involving [(::)] and [(++)] of two lists that have a different
-length as one of its hypotheses. *)
+(** The tactic [discriminate_list] discharges a goal if there is a hypothesis
+[l1 = l2] where [l1] and [l2] have different lengths. The tactic is guaranteed
+to work if [l1] and [l2] contain solely [ [] ], [(::)] and [(++)]. *)
 Tactic Notation "discriminate_list" hyp(H) :=
   apply (f_equal length) in H;
   repeat (csimpl in H || rewrite length_app in H); exfalso; lia.
-- 
GitLab