aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Program/Wf.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Program/Wf.v')
-rw-r--r--theories/Program/Wf.v2
1 files changed, 0 insertions, 2 deletions
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index abab954af..a823aedd3 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -14,8 +14,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.