diff options
Diffstat (limited to 'theories/FSets/OrderedTypeEx.v')
| -rw-r--r-- | theories/FSets/OrderedTypeEx.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/FSets/OrderedTypeEx.v b/theories/FSets/OrderedTypeEx.v index 1ed981f8d9..8da19706e8 100644 --- a/theories/FSets/OrderedTypeEx.v +++ b/theories/FSets/OrderedTypeEx.v @@ -138,7 +138,7 @@ Module Positive_as_OT <: UsualOrderedType. apply GT; unfold lt. replace Eq with (CompOpp Eq); auto. rewrite <- Pcompare_antisym; rewrite H; auto. - Qed. + Defined. End Positive_as_OT. |