From 3b7e7f7738737475cb0f09130b0487c85906dd2b Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Fri, 28 Jul 2017 13:29:36 +0200
Subject: Change the option for cumulativity

---
 test-suite/coqchk/cumulativity.v  | 2 +-
 test-suite/success/cumulativity.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/coqchk/cumulativity.v b/test-suite/coqchk/cumulativity.v
index a978f6b901..7906a5b15e 100644
--- a/test-suite/coqchk/cumulativity.v
+++ b/test-suite/coqchk/cumulativity.v
@@ -1,5 +1,5 @@
 Set Universe Polymorphism.
-Set Inductive Cumulativity.
+Set Polymorphic Inductive Cumulativity.
 Set Printing Universes.
 
 Inductive List (A: Type) := nil | cons : A -> List A -> List A.
diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v
index 8854435cf3..0ee85712e2 100644
--- a/test-suite/success/cumulativity.v
+++ b/test-suite/success/cumulativity.v
@@ -5,7 +5,7 @@ Polymorphic Cumulative Record R1 := { r1 : T1 }.
 Fail Monomorphic Cumulative Inductive R2 := {r2 : T1}.
 
 Set Universe Polymorphism.
-Set Inductive Cumulativity.
+Set Polymorphic Inductive Cumulativity.
 Set Printing Universes.
 
 Inductive List (A: Type) := nil | cons : A -> List A -> List A.
-- 
cgit v1.2.3