diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-01-06 16:51:44 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-01-06 16:55:35 +0100 |
| commit | 352ce04861c5dd849d20832a8fa0379ea8f43c8c (patch) | |
| tree | 09ba5fa82f8b6928623e4eafcff96f47f3829d52 /test-suite/interactive | |
| parent | b4b315107cdf15c1358512c78ebbb5b2c19e8455 (diff) | |
fix simple test for paral-itp
Diffstat (limited to 'test-suite/interactive')
| -rwxr-xr-x | test-suite/interactive/Paral-ITP-demo.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/test-suite/interactive/Paral-ITP-demo.v b/test-suite/interactive/Paral-ITP-demo.v index 5bfa46c2e..0d75d52a3 100755 --- a/test-suite/interactive/Paral-ITP-demo.v +++ b/test-suite/interactive/Paral-ITP-demo.v @@ -53,7 +53,7 @@ Lemma pair_1 : forall (A B : Set) (H : A * B), H = pair (fst H) (snd H). Proof. intros. case H. - introsc. + intros. simpl in |- *. reflexivity. Qed. @@ -66,7 +66,7 @@ Proof. case H1. case H2. simpl in |- *. - introsx. + intros. rewrite H. rewrite H0. reflexivity. @@ -242,7 +242,7 @@ Proof. intro. left. assumption. - introx. + intro. right. apply Zplus_lt_reg_l with (p := x). rewrite Zplus_0_r. |