diff options
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} := |