Skip to content

Commit 4ee8977

Browse files
authored
Merge pull request #11235 from jajimajp/patch-1
[Reference manual/Coq] Fix label for VERNAC EXTEND
2 parents df45715 + 0c68f6a commit 4ee8977

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

doc/coq.rst

+1-1
Original file line numberDiff line numberDiff line change
@@ -723,7 +723,7 @@ reference looks like:
723723
724724
DECLARE PLUGIN "my-coq-plugin.plugin"
725725
726-
VERNAC COMMAND EXTEND CallToC CLASSIFIED AS QUERY
726+
VERNAC COMMAND EXTEND Hello CLASSIFIED AS QUERY
727727
| [ "Hello" ] -> { Feedback.msg_notice Pp.(str Hello_world.hello_world) }
728728
END
729729

0 commit comments

Comments
 (0)