diff options
| author | Clément Pit-Claudel | 2019-03-10 19:00:21 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2019-03-10 19:00:21 -0400 |
| commit | 660732f055021bb4ed3d0a4613aac719cb8f3556 (patch) | |
| tree | 6e5623b6e80e8a356055ad9ea19d63dac6bb39d8 /doc/sphinx/language | |
| parent | 200a1712b9948fa7682dc95eeb0a520d6804caaf (diff) | |
| parent | 9c201fe42142de7332149863d6c1343c2dec8391 (diff) | |
Merge PR #9654: [sphinx] Add warn option to coqtop directive.
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: vbgl
Reviewed-by: cpitclaudel
Diffstat (limited to 'doc/sphinx/language')
| -rw-r--r-- | doc/sphinx/language/coq-library.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 4 |
2 files changed, 6 insertions, 3 deletions
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index c1eab8a970..d1b95e6203 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -606,7 +606,10 @@ Finally, it gives the definition of the usual orderings ``le``, single: ge (term) single: gt (term) -.. coqtop:: in +.. This emits a notation already used warning but it won't be shown to + the user. + +.. coqtop:: in warn Inductive le (n:nat) : nat -> Prop := | le_n : le n n diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 9ab3f905e6..9bd41d79b7 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -1023,7 +1023,7 @@ Mutually defined inductive types .. coqtop:: in - Variables A B : Set. + Parameters A B : Set. Inductive tree : Set := node : A -> forest -> tree @@ -1533,7 +1533,7 @@ the following attributes names are recognized: .. example:: - .. coqtop:: all reset + .. coqtop:: all reset warn From Coq Require Program. #[program] Definition one : nat := S _. |