diff options
Diffstat (limited to 'mathcomp/ssreflect/ssrnat.v')
| -rw-r--r-- | mathcomp/ssreflect/ssrnat.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index 0a2fbcd..dcb518f 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.v @@ -106,6 +106,9 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. +Declare Scope coq_nat_scope. +Declare Scope nat_rec_scope. + (* Disable Coq prelude hints to improve proof script robustness. *) Remove Hints plus_n_O plus_n_Sm mult_n_O mult_n_Sm : core. |