From 8ff2de8c01b3ba3563517627b1f5c9eb2c4bcb77 Mon Sep 17 00:00:00 2001 From: msozeau Date: Wed, 14 Mar 2012 09:53:06 +0000 Subject: Final part of moving Program code inside the main code. Adapted add_definition/fixpoint and parsing of the "Program" prefix. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15036 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/FSets/FMapPositive.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'theories/FSets') diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v index 2e2eb166d..6d0315b82 100644 --- a/theories/FSets/FMapPositive.v +++ b/theories/FSets/FMapPositive.v @@ -494,9 +494,9 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Definition lt_key (p p':positive*A) := E.lt (fst p) (fst p'). - Global Program Instance eqk_equiv : Equivalence eq_key. - Global Program Instance eqke_equiv : Equivalence eq_key_elt. - Global Program Instance ltk_strorder : StrictOrder lt_key. + Global Instance eqk_equiv : Equivalence eq_key := _. + Global Instance eqke_equiv : Equivalence eq_key_elt := _. + Global Instance ltk_strorder : StrictOrder lt_key := _. Lemma mem_find : forall m x, mem x m = match find x m with None => false | _ => true end. -- cgit v1.2.3