diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-12 14:48:05 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-12 14:48:05 +0000 |
| commit | 2482f06c501e43e8aded19e14ae280ec2eab28d5 (patch) | |
| tree | 4b32d6369dfe06bb1dae59233daed7c355297117 /theories | |
| parent | 5e0f9cb6eecc1c02566278ede0cb86ef68a03662 (diff) | |
Bind et Delimit pour R
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4373 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Reals/Rsyntax.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Reals/Rsyntax.v b/theories/Reals/Rsyntax.v index 60a205cfd..771d89852 100644 --- a/theories/Reals/Rsyntax.v +++ b/theories/Reals/Rsyntax.v @@ -244,6 +244,6 @@ Open Local Scope R_scope. End R_scope. ]. -Delimits Scope R_scope with R. - +(* Arguments Scope up [R_scope]. +*) |