diff options
| author |  Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-11 12:46:23 +0200 |
|---|---|---|
| committer | Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-11 12:54:18 +0200 |
| commit | fe99efdbe409e47f20776c62a76d4de7f0188afc (patch) | |
| tree | 6b5566974d82bfa7a285c1dd08508a712360b43e /test-suite/failure | |
| parent | d3a2acc9fceff7476bc2d9eaadab8411365172a2 (diff) | |
Update various comments to use "template polymorphism"
Also remove obvious comments.
Diffstat (limited to 'test-suite/failure')
| -rw-r--r-- | test-suite/failure/proofirrelevance.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/test-suite/failure/proofirrelevance.v b/test-suite/failure/proofirrelevance.v index b62f9b686..bb9579d48 100644 --- a/test-suite/failure/proofirrelevance.v +++ b/test-suite/failure/proofirrelevance.v @@ -1,6 +1,5 @@ -(* This was working in version 8.1beta (bug in the Sort-polymorphism - of inductive types), but this is inconsistent with classical logic - in Prop *) +(* This was working in version 8.1beta (bug in template polymorphism), + but this is inconsistent with classical logic in Prop *) Inductive bool_in_prop : Type := hide : bool -> bool_in_prop with bool : Type := true : bool | false : bool. |