diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-20 10:36:32 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-20 10:36:32 +0000 |
| commit | 94b5cb2a8a10a7e97e8f63ca85d436e983b959a7 (patch) | |
| tree | 9b3080f930c0a5c3f2d12b3a42e97c47974c4d3d /theories/Reals/Rdefinitions.v | |
| parent | f57b6a25082f024bb4c743608c25b7037bf07b8d (diff) | |
R passe dans Set !
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4677 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Rdefinitions.v')
| -rw-r--r-- | theories/Reals/Rdefinitions.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v index c3f3ba5c9..fc1e36631 100644 --- a/theories/Reals/Rdefinitions.v +++ b/theories/Reals/Rdefinitions.v @@ -15,7 +15,7 @@ Require Export ZArith_base. -Parameter R:Type. +Parameter R:Set. (* Declare Scope positive_scope with Key R *) Delimits Scope R_scope with R. |