From 8b5cab33d9877f51a5b3e1f2428c08fd07302352 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 8 Jul 2016 12:04:56 +0200 Subject: Typo in a comment of stdlib. --- theories/Logic/EqdepFacts.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/Logic') diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index 30e26c7c6..bd59159bb 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -164,7 +164,7 @@ Proof. split; auto using eq_sig_eq_dep, eq_dep_eq_sig. Qed. -(** Dependent equality is equivalent tco a dependent pair of equalities *) +(** Dependent equality is equivalent to a dependent pair of equalities *) Set Implicit Arguments. -- cgit v1.2.3