From fc3b7b356e68dba0bbabd8bf755c3a836f6a6396 Mon Sep 17 00:00:00 2001 From: msozeau Date: Sat, 19 Dec 2009 17:58:53 +0000 Subject: 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 --- theories/Sets/Integers.v | 1 + 1 file changed, 1 insertion(+) (limited to 'theories/Sets') 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. -- cgit v1.2.3