From ea19a7f2b5ae99024f6b9345afb993a859b07258 Mon Sep 17 00:00:00 2001 From: whitequark Date: Thu, 21 Jun 2018 12:32:20 +0000 Subject: Fix typo in Init.Logic. --- theories/Init/Logic.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories') diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 817581cb2..9d60cf54c 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -459,7 +459,7 @@ Proof. destruct e. reflexivity. Defined. -(** The goupoid structure of equality *) +(** The groupoid structure of equality *) Theorem eq_trans_refl_l : forall A (x y:A) (e:x=y), eq_trans eq_refl e = e. Proof. -- cgit v1.2.3