diff options
| author | Pierre-Marie Pédrot | 2018-12-20 14:57:17 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-12-20 14:57:17 +0100 |
| commit | 8d41928c9f0bb54ed41e3ab0d7a6f76d556bb588 (patch) | |
| tree | 80cacb02f1e8785c30ce2fd7fe662a5efa1c2cba /test-suite/output/Inductive.v | |
| parent | 525d174b6e6f966e95b3c1f649c8b83ef52abd75 (diff) | |
| parent | 0a25e351d6a2d25e5d82b165843a09a2804fadc6 (diff) | |
Merge PR #8488: Warning when using automatic template polymorphism
Diffstat (limited to 'test-suite/output/Inductive.v')
| -rw-r--r-- | test-suite/output/Inductive.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/output/Inductive.v b/test-suite/output/Inductive.v index 8ff91268a6..9eec9a7dad 100644 --- a/test-suite/output/Inductive.v +++ b/test-suite/output/Inductive.v @@ -3,5 +3,5 @@ Fail Inductive list' (A:Set) : Set := | cons' : A -> list' A -> list' (A*A). (* Check printing of let-ins *) -Inductive foo (A : Type) (x : A) (y := x) := Foo. +#[universes(template)] Inductive foo (A : Type) (x : A) (y := x) := Foo. Print foo. |