MSets: Class Ok becomes a definition instead of an inductive (thanks Matthieu)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12656 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 16 insertions, 23 deletions

diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v
index f7da8bf27..f79f8d0b2 100644
--- a/theories/MSets/MSetAVL.v
+++ b/theories/MSets/MSetAVL.v
@@ -536,7 +536,7 @@ Inductive bst : tree -> Prop :=
 
 Definition IsOk := bst.
 
-Class Ok (s:t) : Prop := { ok : bst s }.
+Class Ok (s:t) : Prop := ok : bst s.
 
 Instance bst_Ok s (Hs : bst s) : Ok s := { ok := Hs }.
 
@@ -576,7 +576,8 @@ Module Import MX := OrderedTypeFacts X.
 Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans @ok.
 Local Hint Immediate MX.eq_sym.
 Local Hint Unfold In lt_tree gt_tree.
-Local Hint Constructors InT bst Ok.
+Local Hint Constructors InT bst.
+Local Hint Unfold Ok.
 
 Tactic Notation "factornode" ident(l) ident(x) ident(r) ident(h)
  "as" ident(s) :=
@@ -585,9 +586,9 @@ Tactic Notation "factornode" ident(l) ident(x) ident(r) ident(h)
 (** Automatic treatment of [Ok] hypothesis *)
 
 Ltac inv_ok := match goal with
- | H:Ok (Node _ _ _ _) |- _ => apply @ok in H; inversion_clear H; inv_ok
+ | H:Ok (Node _ _ _ _) |- _ => inversion_clear H; inv_ok
  | H:Ok Leaf |- _ => clear H; inv_ok
- | H:bst _ |- _ => generalize (Build_Ok H); clear H; intro H; inv_ok
+ | H:bst ?x |- _ => change (Ok x) in H; inv_ok
  | _ => idtac
 end.
 
@@ -665,7 +666,7 @@ Proof. intros; apply <- isok_iff; auto. Qed.
 Lemma In_1 :
  forall s x y, X.eq x y -> InT x s -> InT y s.
 Proof.
- induction s; simpl; intuition_in; eauto 3. (** TODO: why 5 is so slow ? *)
+ induction s; simpl; intuition_in; eauto.
 Qed.
 Local Hint Immediate In_1.
 
diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index 0de28d5e8..ae26fa7ed 100644
--- a/theories/MSets/MSetInterface.v
+++ b/theories/MSets/MSetInterface.v
@@ -340,7 +340,7 @@ Module Type WRawSets (E : DecidableType).
   (** Is a set well-formed or ill-formed ? *)
 
   Parameter IsOk : t -> Prop.
-  Class Ok (s:t) : Prop := { ok : IsOk s }.
+  Class Ok (s:t) : Prop := ok : IsOk s.
 
   (** In order to be able to validate (at least some) particular sets as
       well-formed, we ask for a boolean function for (semi-)deciding
@@ -425,14 +425,6 @@ Module Type WRawSets (E : DecidableType).
 
   End Spec.
 
-(*
- BUG ?! When the Instance *_ok were under a section,
-   this re-export was mandatory !! BUG in Global Instance ?
- Hint Resolve empty_ok add_ok remove_ok union_ok inter_ok
-  diff_ok singleton_ok filter_ok partition_ok1 partition_ok2
-  : typeclass_instances.
-*)
-
 End WRawSets.
 
 (** From weak raw sets to weak usual sets *)
diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v
index b0caf6692..c29742332 100644
--- a/theories/MSets/MSetList.v
+++ b/theories/MSets/MSetList.v
@@ -225,17 +225,17 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
 
   Definition IsOk := Sort.
 
-  Class Ok (s:t) : Prop := { ok : Sort s }.
+  Class Ok (s:t) : Prop := ok : Sort s.
 
   Hint Resolve @ok.
-  Hint Constructors Ok.
+  Hint Unfold Ok.
 
   Instance Sort_Ok s `(Hs : Sort s) : Ok s := { ok := Hs }.
 
   Ltac inv_ok := match goal with
-   | H:Ok (_ :: _) |- _ => apply @ok in H; inversion_clear H; inv_ok
+   | H:Ok (_ :: _) |- _ => inversion_clear H; inv_ok
    | H:Ok nil |- _ => clear H; inv_ok
-   | H:Sort ?l |- _ => generalize (Build_Ok H); clear H; intro H; inv_ok
+   | H:Sort ?l |- _ => change (Ok l) in H; inv_ok
    | _ => idtac
   end.
 
@@ -439,7 +439,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
 
   Global Instance diff_ok s s' `(Ok s, Ok s') : Ok (diff s s').
   Proof.
-  induction2. constructors; auto. apply @ok; auto.
+  induction2. constructors; auto.
   Qed.
 
   Lemma diff_spec :
diff --git a/theories/MSets/MSetWeakList.v b/theories/MSets/MSetWeakList.v
index feab44f58..6b9c17079 100644
--- a/theories/MSets/MSetWeakList.v
+++ b/theories/MSets/MSetWeakList.v
@@ -126,17 +126,17 @@ Module MakeRaw (X:DecidableType) <: WRawSets X.
 
   Definition IsOk := NoDup.
 
-  Class Ok (s:t) : Prop := { ok : NoDup s }.
+  Class Ok (s:t) : Prop := ok : NoDup s.
 
-  Hint Constructors Ok.
+  Hint Unfold Ok.
   Hint Resolve @ok.
 
   Instance NoDup_Ok s (nd : NoDup s) : Ok s := { ok := nd }.
 
   Ltac inv_ok := match goal with
-   | H:Ok (_ :: _) |- _ => apply @ok in H; inversion_clear H; inv_ok
+   | H:Ok (_ :: _) |- _ => inversion_clear H; inv_ok
    | H:Ok nil |- _ => clear H; inv_ok
-   | H:NoDup ?l |- _ => generalize (Build_Ok H); clear H; intro H; inv_ok
+   | H:NoDup ?l |- _ => change (Ok l) in H; inv_ok
    | _ => idtac
   end.