aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/subtac/test/ListsTest.v
diff options
context:
space:
mode:
authorGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-09-17 15:58:14 +0000
committerGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-09-17 15:58:14 +0000
commit61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch)
tree961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /plugins/subtac/test/ListsTest.v
parent6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (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.v18
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.