Fix setoid_rewrite documentation examples.

Debug handling of identifiers in coqdoc (should work with modules and
sections) and add missing macros.
Move theories/Program to THEORIESVO to put the files in the standard
library documentation.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11046 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 7 insertions, 5 deletions

diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index a5e560c89..6a61a16d4 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -21,19 +21,21 @@ Definition id {A} := fun x : A => x.
 
 (** Function composition. *)
 
-Definition compose {A B C} (g : B -> C) (f : A -> B) := fun x : A => g (f x).
+Definition compose {A B C} (g : B -> C) (f : A -> B) := 
+  fun x : A => g (f x).
 
 Hint Unfold compose.
 
-Notation " g ∘ f " := (compose g f)  (at level 40, left associativity) : program_scope.
+Notation " g ∘ f " := (compose g f)  
+  (at level 40, left associativity) : program_scope.
 
 Open Local Scope program_scope.
 
-(** [arrow A B] represents the non-dependent function space between [A] and [B]. *)
+(** The non-dependent function space between [A] and [B]. *)
 
 Definition arrow (A B : Type) := A -> B.
 
-(** [impl A B] represents the logical implication of [B] by [A]. *)
+(** Logical implication. *)
 
 Definition impl (A B : Prop) : Prop := A -> B.
 
@@ -45,7 +47,7 @@ Definition const {A B} (a : A) := fun _ : B => a.
 
 Definition flip {A B C} (f : A -> B -> C) x y := f y x.
 
-(** [apply f x] simply applies [f] to [x]. *)
+(** Application as a combinator. *)
 
 Definition apply {A B} (f : A -> B) (x : A) := f x.