diff options
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 _. |