diff options
Diffstat (limited to 'theories/Numbers/Natural/BigN/BigN.v')
| -rw-r--r-- | theories/Numbers/Natural/BigN/BigN.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v index 40f08356b..4cc867898 100644 --- a/theories/Numbers/Natural/BigN/BigN.v +++ b/theories/Numbers/Natural/BigN/BigN.v @@ -20,14 +20,14 @@ Require Import Cyclic31. Require Import NSig. Require Import NSigNAxioms. Require Import NMake. -Require Import NSub. +Require Import NProperties. Module BigN <: NType := NMake.Make Int31Cyclic. (** Module [BigN] implements [NAxiomsSig] *) Module Export BigNAxiomsMod := NSig_NAxioms BigN. -Module Export BigNSubPropMod := NSubPropFunct BigNAxiomsMod. +Module Export BigNPropMod := NPropFunct BigNAxiomsMod. (** Notations about [BigN] *) @@ -38,7 +38,7 @@ Bind Scope bigN_scope with bigN. Bind Scope bigN_scope with BigN.t. Bind Scope bigN_scope with BigN.t_. -Notation Local "0" := BigN.zero : bigN_scope. (* temporary notation *) +Local Notation "0" := BigN.zero : bigN_scope. (* temporary notation *) Infix "+" := BigN.add : bigN_scope. Infix "-" := BigN.sub : bigN_scope. Infix "*" := BigN.mul : bigN_scope. |