From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Sun, 25 Jan 2015 14:42:51 +0100
Subject: Imported Upstream version 8.5~beta1+dfsg

---
 test-suite/success/TestRefine.v | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'test-suite/success/TestRefine.v')

diff --git a/test-suite/success/TestRefine.v b/test-suite/success/TestRefine.v
index aecc9ed0..3090f40c 100644
--- a/test-suite/success/TestRefine.v
+++ b/test-suite/success/TestRefine.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -53,7 +53,7 @@ Abort.
 
 Lemma essai2 : forall x : nat, x = x.
 
- refine (fix f (x : nat) : x = x := _).
+Fail refine (fix f (x : nat) : x = x := _).
 
 Restart.
 
@@ -119,7 +119,7 @@ Lemma essai : {x : nat | x = 1}.
 Restart.
 
 (* mais si on contraint par le but alors ca marche : *)
-(* Remarque : on peut toujours faire ça *)
+(* Remarque : on peut toujours faire ça *)
  refine (exist _ 1 _:{x : nat | x = 1}).
 
 Restart.
@@ -176,7 +176,7 @@ Restart.
     end).
 
 exists 1. trivial.
-elim (f0 p).
+elim (f p).
  refine
  (fun (x : nat) (h : x = S p) => exist (fun x : nat => x = S (S p)) (S x) _).
  rewrite h. auto.
@@ -184,7 +184,7 @@ Qed.
 
 
 
-(* Quelques essais de recurrence bien fondée *)
+(* Quelques essais de recurrence bien fondée *)
 
 Require Import Wf.
 Require Import Wf_nat.
-- 
cgit v1.2.3