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/Fixpoint.v | |
| parent | 525d174b6e6f966e95b3c1f649c8b83ef52abd75 (diff) | |
| parent | 0a25e351d6a2d25e5d82b165843a09a2804fadc6 (diff) | |
Merge PR #8488: Warning when using automatic template polymorphism
Diffstat (limited to 'test-suite/output/Fixpoint.v')
| -rw-r--r-- | test-suite/output/Fixpoint.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v index 61ae4edbd1..9b25c2dbd3 100644 --- a/test-suite/output/Fixpoint.v +++ b/test-suite/output/Fixpoint.v @@ -44,7 +44,7 @@ fix even_pos_odd_pos 2 with (odd_pos_even_pos n (H:odd n) {struct H} : n >= 1). omega. Qed. -CoInductive Inf := S { projS : Inf }. +#[universes(template)] CoInductive Inf := S { projS : Inf }. Definition expand_Inf (x : Inf) := S (projS x). CoFixpoint inf := S inf. Eval compute in inf. |