From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- theories/Structures/GenericMinMax.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/Structures/GenericMinMax.v') diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v index 05edc6cc..4d04667c 100644 --- a/theories/Structures/GenericMinMax.v +++ b/theories/Structures/GenericMinMax.v @@ -83,7 +83,7 @@ End GenericMinMax. Module MinMaxLogicalProperties (Import O:TotalOrder')(Import M:HasMinMax O). Module Import Private_Tac := !MakeOrderTac O O. -(** An alternative caracterisation of [max], equivalent to +(** An alternative characterisation of [max], equivalent to [max_l /\ max_r] *) Lemma max_spec n m : -- cgit v1.2.3