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

---
 parsing/g_vernac.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'parsing')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 3d29fca77..568818c27 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -169,7 +169,7 @@ GEXTEND Gram
 	  let cum =
 	    match cum with
 	      Some b -> b
-	    | None -> Flags.is_inductive_cumulativity ()
+	    | None -> Flags.is_polymorphic_inductive_cumulativity ()
 	  in
           VernacInductive (cum, priv,f,indl)
       | "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
-- 
cgit v1.2.3