summaryrefslogtreecommitdiff
path: root/theories/Program/Wf.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Program/Wf.v')
-rw-r--r--theories/Program/Wf.v4
1 files changed, 1 insertions, 3 deletions
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index 4159f436..4ca49c41 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -5,7 +5,7 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Wf.v 13332 2010-07-26 22:12:43Z msozeau $ *)
+(* $Id: Wf.v 13492 2010-10-04 21:20:01Z herbelin $ *)
(** Reformulation of the Wf module using subsets where possible, providing
the support for [Program]'s treatment of well-founded definitions. *)
@@ -16,8 +16,6 @@ Require Import ProofIrrelevance.
Open Local Scope program_scope.
-Implicit Arguments Acc_inv [A R x y].
-
Section Well_founded.
Variable A : Type.
Variable R : A -> A -> Prop.