From ae38ce8f2ebe0e82203375fa672de3e91f9dff26 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 3 Dec 2019 12:10:56 +0100
Subject: [PATCH] Fix some Coqdoc.
---
theories/proofmode/ltac_tactics.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 786f912f5..d9ff74e69 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -955,7 +955,7 @@ Ltac iSpecializePat_go H1 pats :=
Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
let pats := spec_pat.parse pat in iSpecializePat_go H pats.
-(* The argument [p] denotes whether the conclusion of the specialized term is
+(** The argument [p] denotes whether the conclusion of the specialized term is
intuitionistic. If so, one can use all spatial hypotheses for both proving the
premises and the remaning goal. The argument [p] can either be a Boolean or an
introduction pattern, which will be coerced into [true] when it solely contains
@@ -2579,7 +2579,7 @@ Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
(** * Assert *)
(* The argument [p] denotes whether [Q] is persistent. It can either be a
Boolean or an introduction pattern, which will be coerced into [true] if it
-only contains `#` or `%` patterns at the top-level, and [false] otherwise. *)
+only contains [#] or [%] patterns at the top-level, and [false] otherwise. *)
Tactic Notation "iAssertCore" open_constr(Q)
"with" constr(Hs) "as" constr(p) tactic3(tac) :=
iStartProof;
--
GitLab