diff --git a/theories/namespaces.v b/theories/namespaces.v index 06927213beccfd10ba7dbd3514a32214bc30127a..04f9e931143bac93cd0465fcf847f923f23aedde 100644 --- a/theories/namespaces.v +++ b/theories/namespaces.v @@ -68,27 +68,27 @@ Section namespace. Proof. intros. by apply symmetry, ndot_preserve_disjoint_l. Qed. End namespace. -(* The hope is that registering these will suffice to solve most goals +(** The hope is that registering these will suffice to solve most goals of the forms: - [N1 ## N2] - [↑N1 ⊆ E ∖ ↑N2 ∖ .. ∖ ↑Nn] - [E1 ∖ ↑N1 ⊆ E2 ∖ ↑N2 ∖ .. ∖ ↑Nn] *) Create HintDb ndisj. -(* Rules for goals of the form [_ ⊆ _] *) -(* If-and-only-if rules. Well, not quite, but for the fragment we are +(** Rules for goals of the form [_ ⊆ _] *) +(** If-and-only-if rules. Well, not quite, but for the fragment we are considering they are. *) Hint Resolve (subseteq_difference_r (A:=positive) (C:=coPset)) : ndisj. Hint Resolve (empty_subseteq (A:=positive) (C:=coPset)) : ndisj. Hint Resolve (union_least (A:=positive) (C:=coPset)) : ndisj. -(* Fallback, loses lots of information but lets other rules make progress. *) +(** Fallback, loses lots of information but lets other rules make progress. *) Hint Resolve (subseteq_difference_l (A:=positive) (C:=coPset)) | 100 : ndisj. Hint Resolve nclose_subseteq' | 100 : ndisj. -(* Rules for goals of the form [_ ## _] *) -(* The base rule that we want to ultimately get down to. *) +(** Rules for goals of the form [_ ## _] *) +(** The base rule that we want to ultimately get down to. *) Hint Extern 0 (_ ## _) => apply ndot_ne_disjoint; congruence : ndisj. -(* Fallback, loses lots of information but lets other rules make progress. +(** Fallback, loses lots of information but lets other rules make progress. Tests show trying [disjoint_difference_l1] first gives better performance. *) Hint Resolve (disjoint_difference_l1 (A:=positive) (C:=coPset)) | 50 : ndisj. Hint Resolve (disjoint_difference_l2 (A:=positive) (C:=coPset)) | 100 : ndisj.