From a28d9981e5baf812de14e62de8d904e545e804e5 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 30 Jun 2015 16:39:26 +0200
Subject: Another missing Fail and comment in test-suite.

---
 test-suite/success/decl_mode2.v | 6 +++---
 1 file 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
-- 
cgit v1.2.3