diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-07-18 11:30:39 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-07-18 11:30:39 +0200 |
| commit | 2042daa9a6e13cbb9636a62812015749d95c2283 (patch) | |
| tree | cbf6e5015eee1ed9ad6792d837dcc63423dee3fd /theories/Init/Wf.v | |
| parent | 8c7ecc85f5535e9d409d51087b1119fe1e61f0cb (diff) | |
Replacing deprecated Implicit Arguments in prelude.
Was triggering a deprecation warning.
Diffstat (limited to 'theories/Init/Wf.v')
| -rw-r--r-- | theories/Init/Wf.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v index 985ecaf27..b5b17e5e8 100644 --- a/theories/Init/Wf.v +++ b/theories/Init/Wf.v @@ -34,7 +34,7 @@ Section Well_founded. destruct 1; trivial. Defined. - Global Implicit Arguments Acc_inv [x y] [x]. + Global Arguments Acc_inv [x] _ [y] _, [x] _ y _. (** A relation is well-founded if every element is accessible *) |