diff options
Diffstat (limited to 'theories/Logic/ConstructiveEpsilon.v')
| -rw-r--r-- | theories/Logic/ConstructiveEpsilon.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v index dc18496f7..70702f486 100644 --- a/theories/Logic/ConstructiveEpsilon.v +++ b/theories/Logic/ConstructiveEpsilon.v @@ -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} := |