diff options
Diffstat (limited to 'theories/Numbers/Natural')
-rw-r--r-- | theories/Numbers/Natural/BigN/BigN.v | 4 | ||||
-rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 12 |
2 files changed, 8 insertions, 8 deletions
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v index 4cc867898..ba457ffb8 100644 --- a/theories/Numbers/Natural/BigN/BigN.v +++ b/theories/Numbers/Natural/BigN/BigN.v @@ -51,11 +51,11 @@ Notation "x > y" := (BigN.lt y x)(only parsing) : bigN_scope. Notation "x >= y" := (BigN.le y x)(only parsing) : bigN_scope. Notation "[ i ]" := (BigN.to_Z i) : bigN_scope. -Open Scope bigN_scope. +Local Open Scope bigN_scope. (** Example of reasoning about [BigN] *) -Theorem succ_pred: forall q:bigN, +Theorem succ_pred: forall q : bigN, 0 < q -> BigN.succ (BigN.pred q) == q. Proof. intros; apply succ_pred. diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v index 2b199858f..49e7d7256 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -20,12 +20,12 @@ Module NSig_NAxioms (N:NType) <: NAxiomsSig. Delimit Scope NumScope with Num. Bind Scope NumScope with N.t. Local Open Scope NumScope. -Notation "[ x ]" := (N.to_Z x) : NumScope. -Infix "==" := N.eq (at level 70) : NumScope. -Notation "0" := N.zero : NumScope. -Infix "+" := N.add : NumScope. -Infix "-" := N.sub : NumScope. -Infix "*" := N.mul : NumScope. +Local Notation "[ x ]" := (N.to_Z x) : NumScope. +Local Infix "==" := N.eq (at level 70) : NumScope. +Local Notation "0" := N.zero : NumScope. +Local Infix "+" := N.add : NumScope. +Local Infix "-" := N.sub : NumScope. +Local Infix "*" := N.mul : NumScope. Hint Rewrite N.spec_0 N.spec_succ N.spec_add N.spec_mul N.spec_pred N.spec_sub : num. |