diff options
Diffstat (limited to 'doc/sphinx/proof-engine/ssreflect-proof-language.rst')
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index b81830f06b..b240cef40c 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -2902,6 +2902,7 @@ pattern will be used to process its instance. Axiom P : nat -> Prop. Axioms eqn leqn : nat -> nat -> bool. + Declare Scope this_scope. Notation "a != b" := (eqn a b) (at level 70) : this_scope. Notation "a <= b" := (leqn a b) (at level 70) : this_scope. Open Scope this_scope. |