aboutsummaryrefslogtreecommitdiff
path: root/theories/Reals/Rminmax.v
AgeCommit message (Collapse)Author
2010-01-07Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders*letouzey
Old stuff DecidableType.v and OrderedType.v stay there and keep their names for the moment, for compatibility. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12641 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-07Rework of GenericMinMax: new axiomatic, split logical/decidable parts, ↵letouzey
Leibniz part Moreover, instantiation like MinMax are now made without redefining generic properties (easier maintenance). We start using inner modules for qualifying (e.g. Z.max_comm). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12638 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-17Reverse order of arguments in min_case_strong for better uniformity (and ↵letouzey
compatibility...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12595 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-03ROrderedType + Rminmax : Coq's Reals can be seen as OrderedType.letouzey
This way we get properties of Rmin / Rmax (almost) for free. TODO: merge Rbasic_fun and Rminmax... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12463 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 13:02:04 +0000