diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /theories/Logic/ConstructiveEpsilon.v | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'theories/Logic/ConstructiveEpsilon.v')
-rw-r--r-- | theories/Logic/ConstructiveEpsilon.v | 14 |
1 files changed, 7 insertions, 7 deletions
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} := |