From ae38a32f1eb7493fed2f4ccca8c4af7c2595a7ac Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Thu, 2 Oct 2014 09:12:47 +0200
Subject: ConstructiveEpsilon: simplify the before_witness type using
 non-uniform parameters.

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

diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v
index dc18496f7a..70702f486b 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} :=
-- 
cgit v1.2.3