diff options
| author | herbelin | 2003-09-12 14:44:07 +0000 |
|---|---|---|
| committer | herbelin | 2003-09-12 14:44:07 +0000 |
| commit | 701b613fd6f5e27cf69584171fb853cbf48f4530 (patch) | |
| tree | f07eb32b456737a1476026cff035b54653e72cd6 | |
| parent | 86fb851af84e7e62d7f8e3825e78d3ad38bbbdfe (diff) | |
Bind et Delimit pour positive et Z (hors section)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4368 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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. |