diff options
author | 2009-09-17 15:58:14 +0000 | |
---|---|---|
committer | 2009-09-17 15:58:14 +0000 | |
commit | 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch) | |
tree | 961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /plugins/subtac/test/ListsTest.v | |
parent | 6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (diff) |
Delete trailing whitespaces in all *.{v,ml*} files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/subtac/test/ListsTest.v')
-rw-r--r-- | plugins/subtac/test/ListsTest.v | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/plugins/subtac/test/ListsTest.v b/plugins/subtac/test/ListsTest.v index 05fc0803f..2cea0841d 100644 --- a/plugins/subtac/test/ListsTest.v +++ b/plugins/subtac/test/ListsTest.v @@ -7,7 +7,7 @@ Set Implicit Arguments. Section Accessors. Variable A : Set. - Program Definition myhd : forall (l : list A | length l <> 0), A := + Program Definition myhd : forall (l : list A | length l <> 0), A := fun l => match l with | nil => ! @@ -34,22 +34,22 @@ Section app. match l with | nil => l' | hd :: tl => hd :: (tl ++ l') - end + end where "x ++ y" := (app x y). Next Obligation. intros. destruct_call app ; program_simpl. Defined. - + Program Lemma app_id_l : forall l : list A, l = nil ++ l. Proof. simpl ; auto. Qed. - + Program Lemma app_id_r : forall l : list A, l = l ++ nil. Proof. - induction l ; simpl in * ; auto. + induction l ; simpl in * ; auto. rewrite <- IHl ; auto. Qed. @@ -61,7 +61,7 @@ Section Nth. Variable A : Set. - Program Fixpoint nth (l : list A) (n : nat | n < length l) { struct l } : A := + Program Fixpoint nth (l : list A) (n : nat | n < length l) { struct l } : A := match n, l with | 0, hd :: _ => hd | S n', _ :: tl => nth tl n' @@ -70,7 +70,7 @@ Section Nth. Next Obligation. Proof. - simpl in *. auto with arith. + simpl in *. auto with arith. Defined. Next Obligation. @@ -78,7 +78,7 @@ Section Nth. inversion H. Qed. - Program Fixpoint nth' (l : list A) (n : nat | n < length l) { struct l } : A := + Program Fixpoint nth' (l : list A) (n : nat | n < length l) { struct l } : A := match l, n with | hd :: _, 0 => hd | _ :: tl, S n' => nth' tl n' @@ -86,7 +86,7 @@ Section Nth. end. Next Obligation. Proof. - simpl in *. auto with arith. + simpl in *. auto with arith. Defined. Next Obligation. |