diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-19 17:58:53 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-19 17:58:53 +0000 |
| commit | fc3b7b356e68dba0bbabd8bf755c3a836f6a6396 (patch) | |
| tree | 6d5b343339c7675924311f1d54a6814d31a16923 /theories/Sets | |
| parent | 3319ae45b302f17c76dd19ff95c9785d9ba04557 (diff) | |
Backtrack on making exact hints for lemmas starting with products
(e.g. transitivity lemmas) and fix bug #2207, avoiding the generation of
useless eta-redexes during type class instance resolution.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12600 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Sets')
| -rw-r--r-- | theories/Sets/Integers.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v index 01d3bda37..15c1b665e 100644 --- a/theories/Sets/Integers.v +++ b/theories/Sets/Integers.v @@ -79,6 +79,7 @@ Section Integers_sect. auto with sets arith. apply Inhabited_intro with (x := 0). apply Integers_defn. + exact le_Order. Defined. Lemma le_total_order : Totally_ordered nat nat_po Integers. |