diff options
Diffstat (limited to 'theories/FSets/FSetBridge.v')
| -rw-r--r-- | theories/FSets/FSetBridge.v | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v index 0622451f..c03fb92e 100644 --- a/theories/FSets/FSetBridge.v +++ b/theories/FSets/FSetBridge.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: FSetBridge.v 10601 2008-02-28 00:20:33Z letouzey $ *) +(* $Id: FSetBridge.v 11699 2008-12-18 11:49:08Z letouzey $ *) (** * Finite sets library *) @@ -20,11 +20,8 @@ Set Firstorder Depth 2. (** * From non-dependent signature [S] to dependent signature [Sdep]. *) -Module DepOfNodep (M: S) <: Sdep with Module E := M.E. - Import M. +Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E. - Module ME := OrderedTypeFacts E. - Definition empty : {s : t | Empty s}. Proof. exists empty; auto with set. @@ -50,7 +47,7 @@ Module DepOfNodep (M: S) <: Sdep with Module E := M.E. Proof. intros; exists (add x s); auto. unfold Add in |- *; intuition. - elim (ME.eq_dec x y); auto. + elim (E.eq_dec x y); auto. intros; right. eapply add_3; eauto. Qed. @@ -68,7 +65,7 @@ Module DepOfNodep (M: S) <: Sdep with Module E := M.E. intros; exists (remove x s); intuition. absurd (In x (remove x s)); auto with set. apply In_1 with y; auto. - elim (ME.eq_dec x y); intros; auto. + elim (E.eq_dec x y); intros; auto. absurd (In x (remove x s)); auto with set. apply In_1 with y; auto. eauto with set. @@ -396,6 +393,8 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. intros; discriminate H. Qed. + Definition eq_dec := equal. + Definition equal (s s' : t) : bool := if equal s s' then true else false. |