diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-07-04 17:11:45 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-07-11 16:27:56 +0200 |
| commit | fbbcea2eda411fbacfafdeec3266a19af17935f3 (patch) | |
| tree | 24c4d298f6a0a5f294518c450d0dc98f59417bd3 /test-suite/output/inference.v | |
| parent | ba7129f547d1f06c7eb67412404445681d22b920 (diff) | |
Deprecate options that were introduced for compatibility with 8.5.
Diffstat (limited to 'test-suite/output/inference.v')
| -rw-r--r-- | test-suite/output/inference.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v index f761a4dc5..73169dae6 100644 --- a/test-suite/output/inference.v +++ b/test-suite/output/inference.v @@ -14,6 +14,7 @@ Definition P (e:option L) := Print P. (* Check that plus is folded even if reduction is involved *) +Set Warnings Append "-deprecated-option". Set Refolding Reduction. Check (fun m n p (H : S m <= (S n) + p) => le_S_n _ _ H). |