From da882cfdac822da8d53e8c11b4a890e1643901ad Mon Sep 17 00:00:00 2001 From: msozeau Date: Tue, 1 Dec 2009 16:36:52 +0000 Subject: Fix make_exact_entry to allow applying [forall x, P x] hints directly, avoiding the introduction of eta-redexes. Prioritize hints over intros in typeclass resolution to profit from that. Add a minor fix in coqdoc by F. Garillot. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12550 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Sets/Integers.v | 1 - 1 file changed, 1 deletion(-) (limited to 'theories/Sets') diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v index 443713211..01d3bda37 100644 --- a/theories/Sets/Integers.v +++ b/theories/Sets/Integers.v @@ -79,7 +79,6 @@ 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