diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-04-17 11:30:23 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-04-17 11:30:23 +0000 |
| commit | cc1be0bf512b421336e81099aa6906ca47e4257a (patch) | |
| tree | c25fa8ed965729d7a85efa3b3292fdf7f442963d /theories/Lists/Streams.v | |
| parent | ebf9aa9f97ef0d49ed1b799c9213f78efad4fec7 (diff) | |
Uniformisation (Qed/Save et Implicits Arguments)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2650 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Lists/Streams.v')
| -rwxr-xr-x | theories/Lists/Streams.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v index f5f15d889..d63fcac2b 100755 --- a/theories/Lists/Streams.v +++ b/theories/Lists/Streams.v @@ -43,7 +43,7 @@ Qed. Lemma tl_nth_tl : (n:nat)(s:Stream)(tl (Str_nth_tl n s))=(Str_nth_tl n (tl s)). Proof. Induction n; Simpl; Auto. -Save. +Qed. Hints Resolve tl_nth_tl : datatypes v62. Lemma Str_nth_tl_plus @@ -51,12 +51,12 @@ Lemma Str_nth_tl_plus Induction n; Simpl; Intros; Auto with datatypes. Rewrite <- H. Rewrite tl_nth_tl; Trivial with datatypes. -Save. +Qed. Lemma Str_nth_plus : (n,m:nat)(s:Stream)(Str_nth n (Str_nth_tl m s))=(Str_nth (plus n m) s). Intros; Unfold Str_nth; Rewrite Str_nth_tl_plus; Trivial with datatypes. -Save. +Qed. (** Extensional Equality between two streams *) |