diff options
| author | Théo Zimmermann | 2019-02-26 16:33:08 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-02-28 14:26:41 +0100 |
| commit | 9c201fe42142de7332149863d6c1343c2dec8391 (patch) | |
| tree | c97b2599ade286f79c88d07f335f215112fc0018 /doc/sphinx/user-extensions | |
| parent | 9d6f268723b6352a97bcc3baf0df57f1c1b251fa (diff) | |
[sphinx] Add warn option to coqtop directive.
By default Coq warnings are made fatal when building the manual.
If you want to show a command resulting in a warning, use the warn
option.
Preexisting warnings are either fixed or marked as expected.
Diffstat (limited to 'doc/sphinx/user-extensions')
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 4f46a80dcf..e5eb7eb4f5 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1115,6 +1115,8 @@ Binding arguments of a constant to an interpretation scope .. coqtop:: all Parameter g : bool -> bool. + Declare Scope mybool_scope. + Notation "@@" := true (only parsing) : bool_scope. Notation "@@" := false (only parsing): mybool_scope. @@ -1151,6 +1153,7 @@ Binding types of arguments to an interpretation scope .. coqtop:: in reset Parameter U : Set. + Declare Scope U_scope. Bind Scope U_scope with U. Parameter Uplus : U -> U -> U. Parameter P : forall T:Set, T -> U -> Prop. @@ -1575,7 +1578,7 @@ Numeral notations For example - .. coqtop:: all + .. coqtop:: all warn Check 90000. |