From 2f68b37beb32addaabe7b72dede2edf48055cdb3 Mon Sep 17 00:00:00 2001 From: letouzey Date: Mon, 5 Jul 2010 10:09:18 +0000 Subject: FSets/Msets: some renaming of module params to simplify the task of the extraction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13239 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/FSets/FSetBridge.v | 7 ++++--- theories/FSets/FSetCompat.v | 8 ++++---- theories/MSets/MSetInterface.v | 6 +++--- 3 files changed, 11 insertions(+), 10 deletions(-) (limited to 'theories') diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v index 8d6ca420b..25ce5577e 100644 --- a/theories/FSets/FSetBridge.v +++ b/theories/FSets/FSetBridge.v @@ -321,8 +321,6 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E. exists e; unfold For_all in |- *; eauto. Qed. - Module E := E. - Definition elt := elt. Definition t := t. @@ -346,6 +344,8 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E. Definition lt_not_eq := lt_not_eq. Definition compare := compare. + Module E := E. + End DepOfNodep. @@ -783,7 +783,6 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. Qed. - Module E := E. Definition elt := elt. Definition t := t. @@ -809,4 +808,6 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. Definition lt_not_eq := lt_not_eq. Definition compare := compare. + Module E := E. + End NodepOfDep. diff --git a/theories/FSets/FSetCompat.v b/theories/FSets/FSetCompat.v index 439f0e528..c3d614eeb 100644 --- a/theories/FSets/FSetCompat.v +++ b/theories/FSets/FSetCompat.v @@ -173,8 +173,6 @@ Module Backport_Sets Include Backport_WSets E M. - Module E := E. - Implicit Type s : t. Implicit Type x y : elt. @@ -213,6 +211,8 @@ Module Backport_Sets [ apply EQ | apply LT | apply GT ]; auto. Defined. + Module E := E. + End Backport_Sets. @@ -346,8 +346,6 @@ Module Update_Sets with Definition E.lt := E.lt) <: MSetInterface.Sets with Module E:=E. - Module E := E. - Include Update_WSets E M. Implicit Type s : t. @@ -407,4 +405,6 @@ Module Update_Sets Lemma compare_spec : forall s s', CompSpec eq lt s s' (compare s s'). Proof. intros; unfold compare; destruct M.compare; auto. Qed. + Module E := E. + End Update_Sets. diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v index 6de91dacc..851237d8f 100644 --- a/theories/MSets/MSetInterface.v +++ b/theories/MSets/MSetInterface.v @@ -545,9 +545,9 @@ Module WRaw2SetsOn (E:DecidableType)(M:WRawSets E) <: WSetsOn E. End WRaw2SetsOn. -Module WRaw2Sets (E:DecidableType)(M:WRawSets E) <: WSets with Module E := E. - Module E := E. - Include WRaw2SetsOn E M. +Module WRaw2Sets (D:DecidableType)(M:WRawSets D) <: WSets with Module E := D. + Module E := D. + Include WRaw2SetsOn D M. End WRaw2Sets. (** Same approach for ordered sets *) -- cgit v1.2.3