From a445420291a91504665874dfe5b63d9492cf4c73 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sat, 11 Feb 2006 19:40:49 +0000
Subject: Commentaires et compatibilité coqdoc
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8026 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Strings/Ascii.v  | 28 +++++++++++++++++++---------
 theories/Strings/String.v | 32 +++++++++++++++++---------------
 2 files changed, 36 insertions(+), 24 deletions(-)

(limited to 'theories/Strings')

diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v
index 18aaa2c0b..3c0a9667f 100644
--- a/theories/Strings/Ascii.v
+++ b/theories/Strings/Ascii.v
@@ -14,9 +14,7 @@
 Require Import Bool.
 Require Import BinPos.
 
-(***********************************)
-(** Definition of ascii characters *)
-(***********************************)
+(** *** Definition of ascii characters *)
 
 (* Definition of ascii character as a 8 bits constructor *)
  
@@ -53,9 +51,7 @@ Definition ascii_dec : forall a b : ascii, {a = b} + {a <> b}.
  decide equality; apply bool_dec.
 Defined.
 
-(***********************************************************************)
-(** Conversion between natural numbers modulo 256 and ascii characters *)
-(***********************************************************************)
+(** *** Conversion between natural numbers modulo 256 and ascii characters *)
 
 (* Auxillary function that turns a positive into an ascii by
    looking at the last n bits, ie z mod 2^n *)
@@ -112,9 +108,23 @@ Proof.
   destruct a as [[|][|][|][|][|][|][|][|]]; compute; reflexivity.
 Abort.
 
-(********************************)
-(** Examples of concrete syntax *)
-(********************************)
+(** *** Concrete syntax *)
+
+(**
+  Ascii characters can be represented in scope char_scope as follows:
+  - ["c"]   represents itself if c is a character of code < 128,
+  - [""""]  is an exception: it represents the ascii character 34
+            (double quote),
+  - ["nnn"] represents the ascii character of decimal code nnn.
+
+  For instance, both ["065"] and ["A"] denote the character `uppercase
+  A', and both ["034"] and [""""] denote the character `double quote'.
+
+  Notice that the ascii characters of code >= 128 do not denote
+  stand-alone utf8 characters so that only the notation "nnn" is
+  available for them (unless your terminal is able to represent them,
+  which is typically not the case in coqide). 
+*)
 
 Open Local Scope char_scope.
 
diff --git a/theories/Strings/String.v b/theories/Strings/String.v
index 82da318c5..4057ba022 100644
--- a/theories/Strings/String.v
+++ b/theories/Strings/String.v
@@ -14,9 +14,7 @@
 Require Import Arith.
 Require Import Ascii.
 
-(******************************)
-(** Definition of strings     *)
-(******************************)
+(** *** Definition of strings *)
 
 (** Implementation of string as list of ascii characters *)
  
@@ -34,9 +32,7 @@ Definition string_dec : forall s1 s2 : string, {s1 = s2} + {s1 <> s2}.
  decide equality; apply ascii_dec.
 Defined.
 
-(******************************)
-(** Concatenation of strings  *)
-(******************************)
+(** *** Concatenation of strings *)
 
 Reserved Notation "x ++ y" (right associativity, at level 60).
 
@@ -118,9 +114,7 @@ generalize (Rec s2 0); simpl in |- *; auto.
 intros n0; rewrite <- Plus.plus_Snm_nSm; auto.
 Qed.
 
-(******************************)
-(** Substrings                *)
-(******************************)
+(** *** Substrings *)
 
 (** [substring n m s] returns the substring of [s] that starts
     at position [n] and of length [m];
@@ -169,9 +163,7 @@ intros n0 H; apply Rec; simpl in |- *; auto.
 apply Le.le_S_n; auto.
 Qed.
 
-(******************************)
-(** Test functions            *)
-(******************************)
+(** *** Test functions *)
 
 (** Test if [s1] is a prefix of [s2] *)
  
@@ -382,9 +374,19 @@ Definition findex n s1 s2 :=
   | None => 0
   end.
 
-(********************************)
-(** Examples of concrete syntax *)
-(********************************)
+(** *** Concrete syntax *)
+
+(**
+  The concrete syntax for strings in scope string_scope follows the
+  Coq convention for strings: all ascii characters of code less than
+  128 are litteral to the exception of the character `double quote'
+  which must be doubled.
+
+  Strings that involve ascii characters of code >= 128 which are not
+  part of a valid utf8 sequence of characters are not representable
+  using the Coq string notation (use explicitly the String constructor
+  with the ascii codes of the characters).
+*)
 
 Example HelloWorld := "	""Hello world!""
 ".
-- 
cgit v1.2.3