From fe99efdbe409e47f20776c62a76d4de7f0188afc Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Tue, 11 Apr 2017 12:46:23 +0200
Subject: Update various comments to use "template polymorphism"

Also remove obvious comments.
---
 test-suite/failure/proofirrelevance.v | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'test-suite/failure')

diff --git a/test-suite/failure/proofirrelevance.v b/test-suite/failure/proofirrelevance.v
index b62f9b6867..bb9579d487 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.
-- 
cgit v1.2.3