Another missing Fail and comment in test-suite.

1 files changed, 3 insertions, 3 deletions

diff --git a/test-suite/success/decl_mode2.v b/test-suite/success/decl_mode2.v
index edee439f00..3ed622bf7f 100644
--- a/test-suite/success/decl_mode2.v
+++ b/test-suite/success/decl_mode2.v
@@ -146,7 +146,7 @@ Abort.
 Theorem T: forall (P:nat -> Prop), forall x, P x -> P x.
 proof.
 let P:(nat -> Prop).
-let x. (* fails because x's type is not clear *) 
+Fail let x. (* fails because x's type is not clear *) 
 let x be such that HP:(P x). (* here x's type is inferred from (P x) *)
 Abort.
 
@@ -169,7 +169,7 @@ let P:(nat -> Prop),A:Prop be such that H:(exists x, P x /\ A).
 consider x such that HP:(P x) and HA:A from H.
 Abort.
 
-Here is an example with pairs:
+(* Here is an example with pairs: *)
 
 Theorem T: forall p:(nat * nat)%type, (fst p >= snd p) \/ (fst p < snd p).
 proof.
@@ -243,4 +243,4 @@ suppose it is (S m) and H:thesis for m.
   then (S (m + 0) = S m).
   thus =~ (S m + 0).
 end induction.
-Abort.
+Abort.
\ No newline at end of file