aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Structures/GenericMinMax.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Structures/GenericMinMax.v')
-rw-r--r--theories/Structures/GenericMinMax.v7
1 files changed, 1 insertions, 6 deletions
diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v
index 0650546a5..f5ff27888 100644
--- a/theories/Structures/GenericMinMax.v
+++ b/theories/Structures/GenericMinMax.v
@@ -488,7 +488,7 @@ End MinMaxProperties.
-(** Some Remaining questions...
+(** TODO: Some Remaining questions...
--> Compare with a type-classes version ?
@@ -497,9 +497,4 @@ End MinMaxProperties.
--> Is it possible to avoid copy-paste about min even more ?
---> Can this modular approach be used for more complex things,
- in particular div/mod ?
- How can we share common parts between nat and Z in this case ?
- How to handle different choices (Zdiv vs. ZOdiv) ?
-
*)