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

---
 theories/Logic/ConstructiveEpsilon.v | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'theories/Logic/ConstructiveEpsilon.v')

diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v
index 7403208a..6f5bfae4 100644
--- a/theories/Logic/ConstructiveEpsilon.v
+++ b/theories/Logic/ConstructiveEpsilon.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        *)
@@ -51,9 +51,9 @@ Hypothesis P_dec : forall n, {P n}+{~(P n)}.
 any number before any witness (not necessarily the [x] of [exists x :A, P x])
 makes the search eventually stops. *)
 
-Inductive before_witness : nat -> Prop :=
-  | stop : forall n, P n -> before_witness n
-  | next : forall n, before_witness (S n) -> before_witness n.
+Inductive before_witness (n:nat) : Prop :=
+  | stop : P n -> before_witness n
+  | next : before_witness (S n) -> before_witness n.
 
 (* Computation of the initial termination certificate *)
 Fixpoint O_witness (n : nat) : before_witness n -> before_witness 0 :=
@@ -67,9 +67,9 @@ is structurally smaller even in the [stop] case. *)
 Definition inv_before_witness :
   forall n, before_witness n -> ~(P n) -> before_witness (S n) :=
   fun n b =>
-    match b in before_witness n return ~ P n -> before_witness (S n) with
-      | stop n p => fun not_p => match (not_p p) with end
-      | next n b => fun _ => b
+    match b return ~ P n -> before_witness (S n) with
+      | stop _ p => fun not_p => match (not_p p) with end
+      | next _ b => fun _ => b
     end.
 
 Fixpoint linear_search m (b : before_witness m) : {n : nat | P n} :=
-- 
cgit v1.2.3