From 5695ee20ed7d7e5e29219b7b3a895b712c131d0e Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Thu, 20 Jun 2019 20:36:33 +0200 Subject: [PATCH] coqdoc++ --- theories/namespaces.v | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/theories/namespaces.v b/theories/namespaces.v index 0692721..04f9e93 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. -- GitLab