diff options
Diffstat (limited to 'doc/sphinx/language/core/assumptions.rst')
| -rw-r--r-- | doc/sphinx/language/core/assumptions.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/language/core/assumptions.rst b/doc/sphinx/language/core/assumptions.rst index a38282d41a..e029068630 100644 --- a/doc/sphinx/language/core/assumptions.rst +++ b/doc/sphinx/language/core/assumptions.rst @@ -117,7 +117,7 @@ Assumptions Assumptions extend the environment with axioms, parameters, hypotheses or variables. An assumption binds an :n:`@ident` to a :n:`@type`. It is accepted -by |Coq| if and only if this :n:`@type` is a correct type in the environment +by Coq if and only if this :n:`@type` is a correct type in the environment preexisting the declaration and if :n:`@ident` was not previously defined in the same module. This :n:`@type` is considered to be the type (or specification, or statement) assumed by :n:`@ident` and we say that :n:`@ident` |