diff options
| -rw-r--r-- | theories/Structures/OrderedType2.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Structures/OrderedType2.v b/theories/Structures/OrderedType2.v index 14e946dd0..25cfd3b1a 100644 --- a/theories/Structures/OrderedType2.v +++ b/theories/Structures/OrderedType2.v @@ -251,7 +251,7 @@ Ltac order_loop := intros; trivial; | H : x <= z |- _ => fail 1 | _ => generalize (le_trans H1 H2); intro; order_loop end - | _ => auto; fail + | _ => auto end. Ltac order := order_loop; fail. |