diff options
Diffstat (limited to 'theories/Structures/GenericMinMax.v')
| -rw-r--r-- | theories/Structures/GenericMinMax.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v index a0ee4caaa..ac52d1bbb 100644 --- a/theories/Structures/GenericMinMax.v +++ b/theories/Structures/GenericMinMax.v @@ -110,7 +110,7 @@ Proof. intros x x' Hx y y' Hy. assert (H1 := max_spec x y). assert (H2 := max_spec x' y'). set (m := max x y) in *; set (m' := max x' y') in *; clearbody m m'. - rewrite <- Hx, <- Hy in *. + rewrite <- Hx, <- Hy in *. destruct (lt_total x y); intuition order. Qed. |