Commentaires

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

2 files changed, 20 insertions, 47 deletions

diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 333a35500..2c6addf3d 100755
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -85,9 +85,9 @@ Section Projections.
      Then [(projS1 y)] is the witness [a]
      and [(projS2 y)] is the proof of [(P a)] *)
 
-  Definition projS1 (* : (A:Set)(P:A->Set)(sigS A P) -> A *)
+  Definition projS1 : (sigS A P) -> A
            := [x:(sigS A P)]Cases x of (existS a _) => a end.
-  Definition projS2 (* : (A:Set)(P:A->Set)(H:(sigS A P))(P (projS1 A P H)) *)
+  Definition projS2 : (x:(sigS A P))(P (projS1 x))
            := [x:(sigS A P)]<[x:(sigS A P)](P (projS1 x))> 
                   Cases x of (existS _ h) => h end.
 
@@ -194,10 +194,10 @@ Section projections_sigT.
   Variable A:Type.
   Variable P:A->Type.
 
-  Definition projT1 (* : (A:Type)(P:A->Type)(sigT A P) -> A *)
+  Definition projT1 : (sigT A P) -> A
               := [H:(sigT A P)]Cases H of (existT x _) => x end.
    
-  Definition projT2 (* : (A:Type)(P:A->Type)(p:(sigT A P))(P (projT1 A P p)) *)
+  Definition projT2 : (x:(sigT A P))(P (projT1 x))
               := [H:(sigT A P)]<[H:(sigT A P)](P (projT1 H))> 
                      Cases H of (existT x h) => h end.
 
diff --git a/theories/Lists/TheoryList.v b/theories/Lists/TheoryList.v
index 897996670..c7abe31da 100755
--- a/theories/Lists/TheoryList.v
+++ b/theories/Lists/TheoryList.v
@@ -37,11 +37,10 @@ Hints Resolve Isnil_nil not_Isnil_cons.
 Lemma Isnil_dec : (l:(list A)){(Isnil l)}+{~(Isnil l)}.
 Intro l; Case l;Auto.
 (*
-Realizer [l:(list A)]Cases l of
+Realizer (fun l => match l with
   | nil => true
   | _ => false
-  end.
-Program_all.
+  end).
 *)
 Qed.
 
@@ -54,11 +53,10 @@ Intro l; Case l.
 Auto.
 Intros a m; Intros; Left; Exists a; Exists m; Reflexivity.
 (*
-Realizer [l:(list A)]<(Exc A*(list A))>Cases l of 
-  | nil => Error
-  | (cons a m) => (Value (a,m))
-  end.
-Program_all.
+Realizer (fun l => match l with
+  | nil => error
+  | (cons a m) => value (a,m)
+  end).
 *)
 Qed.
 
@@ -71,12 +69,10 @@ Intro l; Case l.
 Auto.
 Intros a m; Intros; Left; Exists a; Exists m; Reflexivity.
 (*
-Realizer [l:(list A)]<(Exc A)>Cases l of 
-  | nil => Error
-  | (cons a m) => (Value a)
-  end.
-Program_all.
-Exists m; Reflexivity.
+Realizer (fun l => match l with
+  | nil => error
+  | (cons a m) => value a
+  end).
 *)
 Qed.
 
@@ -86,12 +82,10 @@ Intro l; Case l.
 Exists (nil A); Auto.
 Intros a m; Intros; Exists m; Left; Exists a; Reflexivity.
 (*
-Realizer [l:(list A)]Cases l of 
-  | nil => (nil A)
+Realizer (fun l => match l with
+  | nil => nil
   | (cons a m) => m
-  end.
-Program_all.
-  Left; Exists a; Auto.
+  end).
 *)
 Qed.
 
@@ -99,7 +93,7 @@ Qed.
 (** Length of lists                     *)
 (****************************************)
 
-(* length is defined in PolyList *)
+(* length is defined in List *)
 Fixpoint Length_l [l:(list A)] : nat -> nat 
   :=  [n:nat] Cases l of
                   nil => n
@@ -114,17 +108,13 @@ Intro n; Elim (lrec (S n)); Simpl; Intros.
 Exists x; Transitivity (S (plus n (length m))); Auto.
 (*
 Realizer Length_l.
-Program_all.
-Simpl; Auto.
-Elim e; Simpl; Auto.
 *)
 Qed.
 
 Lemma Length : (l:(list A)){m:nat|(length l)=m}.
 Intro l. Apply (Length_l_pf l O).
 (*
-Realizer [l:(list A)](Length_l_pf l O).
-Program_all.
+Realizer (fun l -> Length_l_pf l O).
 *)
 Qed.
 
@@ -170,7 +160,6 @@ Auto.
 Simpl. Elim IHl; Auto.
 (*
 Realizer mem.
-Program_all.
 *)
 Qed.
 
@@ -224,12 +213,8 @@ Left; Exists b; Auto.
 Right; NewDestruct o.
 Absurd (S n1)=O; Auto.
 Auto with arith.
-
 (*
 Realizer Nth_func.
-Program_all.
-Simpl; Elim n; Auto with arith.
-(Elim o; Intro); [Absurd ((S p)=O); Auto with arith | Auto with arith].
 *)
 Qed.
 
@@ -267,18 +252,11 @@ Qed.
 Lemma Index : (a:A)(l:(list A))
      {n:nat|(fst_nth_spec l n a)}+{(AllS [b:A]~a=b l)}.
 
-(*
-Refine [a,l]if (Index_p a l (S O)) then [n,p](left ? ? (exists ? ? n ?)) 
-            else (right ? ? ?).
-*)
-
 Intros a l; Case (Index_p a l (S O)); Auto.
 Intros (n,P); Left; Exists n; Auto.
 Rewrite (minus_n_O n); Trivial.
-
 (*
-Realizer [a:A][l:(list A)](Index_p a l (S O)).
-Program_all.
+Realizer (fun a l -> Index_p a l (S O)).
 *)
 Qed.
 
@@ -331,7 +309,6 @@ Left; Exists a; Auto.
 Auto.
 (*
 Realizer find.
-Program_all.
 *)
 Qed.
 
@@ -358,12 +335,9 @@ NewDestruct (TS_dec a) as [[c H1]|].
 Left; Exists c.
 Exists a; Auto.
 Auto.
-
 (* 
 Realizer try_find.
-Program_all.
 *)
-
 Qed.
 
 End Find_sec.
@@ -399,7 +373,6 @@ Left; Exact b'.
 Right; Auto.
 (*
 Realizer assoc.
-Program_all.
 *)
 Qed.