diff options
Diffstat (limited to 'lib/HashedSet.v')
| -rw-r--r-- | lib/HashedSet.v | 38 |
1 files changed, 19 insertions, 19 deletions
diff --git a/lib/HashedSet.v b/lib/HashedSet.v index cb2ee1b2..48798a1b 100644 --- a/lib/HashedSet.v +++ b/lib/HashedSet.v @@ -118,7 +118,7 @@ Proof. destruct i; simpl; reflexivity. Qed. -Hint Resolve gempty : pset. +Global Hint Resolve gempty : pset. Hint Rewrite gempty : pset. Definition node (b0 : pset) (f : bool) (b1 : pset) : pset := @@ -139,7 +139,7 @@ Proof. all: reflexivity. Qed. -Hint Resolve wf_node: pset. +Global Hint Resolve wf_node: pset. Lemma gnode : forall b0 f b1 i, @@ -180,7 +180,7 @@ Proof. Qed. Hint Rewrite add_nonempty : pset. -Hint Resolve add_nonempty : pset. +Global Hint Resolve add_nonempty : pset. Lemma wf_add: forall i s, (iswf s) -> (iswf (add i s)). @@ -194,7 +194,7 @@ Proof. all: intuition. Qed. -Hint Resolve wf_add : pset. +Global Hint Resolve wf_add : pset. Theorem gadds : forall i : positive, @@ -204,7 +204,7 @@ Proof. induction i; destruct s; simpl; auto. Qed. -Hint Resolve gadds : pset. +Global Hint Resolve gadds : pset. Hint Rewrite gadds : pset. Theorem gaddo : @@ -220,7 +220,7 @@ Proof. all: apply gempty. Qed. -Hint Resolve gaddo : pset. +Global Hint Resolve gaddo : pset. Fixpoint remove (i : positive) (s : pset) { struct i } : pset := match i with @@ -290,7 +290,7 @@ Proof. Qed. Hint Rewrite remove_empty : pset. -Hint Resolve remove_empty : pset. +Global Hint Resolve remove_empty : pset. Lemma gremove_noncanon_s : forall i : positive, @@ -310,7 +310,7 @@ Proof. apply gremove_noncanon_s. Qed. -Hint Resolve gremoves : pset. +Global Hint Resolve gremoves : pset. Hint Rewrite gremoves : pset. Lemma gremove_noncanon_o : @@ -337,7 +337,7 @@ Proof. assumption. Qed. -Hint Resolve gremoveo : pset. +Global Hint Resolve gremoveo : pset. Fixpoint union_nonopt (s s' : pset) : pset := match s, s' with @@ -382,7 +382,7 @@ Proof. all: destruct pset_eq; simpl; trivial; discriminate. Qed. -Hint Resolve union_nonempty1 union_nonempty2 : pset. +Global Hint Resolve union_nonempty1 union_nonempty2 : pset. Lemma wf_union : forall s s', (iswf s) -> (iswf s') -> (iswf (union s s')). @@ -403,7 +403,7 @@ Proof. intuition auto with pset. Qed. -Hint Resolve wf_union : pset. +Global Hint Resolve wf_union : pset. Theorem gunion: forall s s' : pset, @@ -463,7 +463,7 @@ Proof. intuition. Qed. -Hint Resolve wf_inter : pset. +Global Hint Resolve wf_inter : pset. Lemma inter_noncanon_same: forall s s' j, (contains (inter s s') j) = (contains (inter_noncanon s s') j). @@ -483,7 +483,7 @@ Proof. apply ginter_noncanon. Qed. -Hint Resolve ginter gunion : pset. +Global Hint Resolve ginter gunion : pset. Hint Rewrite ginter gunion : pset. Fixpoint subtract_noncanon (s s' : pset) : pset := @@ -535,7 +535,7 @@ Proof. intuition. Qed. -Hint Resolve wf_subtract : pset. +Global Hint Resolve wf_subtract : pset. Lemma subtract_noncanon_same: forall s s' j, (contains (subtract s s') j) = (contains (subtract_noncanon s s') j). @@ -555,7 +555,7 @@ Proof. apply gsubtract_noncanon. Qed. -Hint Resolve gsubtract : pset. +Global Hint Resolve gsubtract : pset. Hint Rewrite gsubtract : pset. Lemma wf_is_nonempty : @@ -585,7 +585,7 @@ Proof. assumption. Qed. -Hint Resolve wf_is_nonempty : pset. +Global Hint Resolve wf_is_nonempty : pset. Lemma wf_is_empty1 : forall s, iswf s -> (forall i, (contains s i) = false) -> is_empty s = true. @@ -618,7 +618,7 @@ Proof. assumption. Qed. -Hint Resolve wf_is_empty1 : pset. +Global Hint Resolve wf_is_empty1 : pset. Lemma wf_eq : forall s s', iswf s -> iswf s' -> s <> s' -> @@ -1376,7 +1376,7 @@ Proof. all: assumption. Qed. -Hint Resolve is_subset_spec1 is_subset_spec2 : pset. +Global Hint Resolve is_subset_spec1 is_subset_spec2 : pset. Theorem is_subset_spec: forall s s', @@ -1409,6 +1409,6 @@ Proof. Qed. End PSet. -Hint Resolve PSet.gaddo PSet.gadds PSet.gremoveo PSet.gremoves PSet.gunion PSet.ginter PSet.gsubtract PSet.gfilter PSet.is_subset_spec1 PSet.is_subset_spec2 : pset. +Global Hint Resolve PSet.gaddo PSet.gadds PSet.gremoveo PSet.gremoves PSet.gunion PSet.ginter PSet.gsubtract PSet.gfilter PSet.is_subset_spec1 PSet.is_subset_spec2 : pset. Hint Rewrite PSet.gadds PSet.gremoves PSet.gunion PSet.ginter PSet.gsubtract PSet.gfilter : pset. |