diff options
| -rw-r--r-- | theories/ZArith/Zsyntax.v | 5 | ||||
| -rw-r--r-- | theories/ZArith/fast_integer.v | 13 |
2 files changed, 14 insertions, 4 deletions
diff --git a/theories/ZArith/Zsyntax.v b/theories/ZArith/Zsyntax.v index 24fd54266c..3c4ed1e3c8 100644 --- a/theories/ZArith/Zsyntax.v +++ b/theories/ZArith/Zsyntax.v @@ -273,8 +273,7 @@ End Z_scope. (* Declare Scope positive_scope with Key P. *) -Delimits Scope positive_scope with P. -Delimits Scope Z_scope with Z. - +(* Arguments Scope POS [positive_scope]. Arguments Scope NEG [positive_scope]. +*) diff --git a/theories/ZArith/fast_integer.v b/theories/ZArith/fast_integer.v index 334dc050fb..cb0a2b9935 100644 --- a/theories/ZArith/fast_integer.v +++ b/theories/ZArith/fast_integer.v @@ -17,16 +17,27 @@ Require Mult. Require Minus. (** Definition of fast binary integers *) -Section fast_integers. Inductive positive : Set := xI : positive -> positive | xO : positive -> positive | xH : positive. +Delimits Scope positive_scope with P. +Delimits Scope Z_scope with Z. +Arguments Scope xO [ positive_scope ]. +Arguments Scope xI [ positive_scope ]. + Inductive Z : Set := ZERO : Z | POS : positive -> Z | NEG : positive -> Z. +Bind Scope positive_scope with positive. +Bind Scope Z_scope with Z. +Arguments Scope POS [ Z_scope ]. +Arguments Scope NEG [ Z_scope ]. + +Section fast_integers. + Inductive relation : Set := EGAL :relation | INFERIEUR : relation | SUPERIEUR : relation. |