From 55e62174683f293c8f966d8bd486fcb511f66221 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <mattam@mattam.org>
Date: Wed, 11 Dec 2013 17:19:01 +0000
Subject: - Fix handling of polymorphic inductive elimination schemes. - Avoid
 generation of dummy universes for unsafe_global* - Handle side effects better
 for polymorphic definitions.

Conflicts:
	kernel/term_typing.ml
	tactics/tactics.ml
---
 toplevel/vernacentries.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'toplevel')

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 450b6ee51..bb702f79f 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1838,7 +1838,8 @@ let check_vernac_supports_locality c l =
     | VernacSetOpacity _ | VernacSetStrategy _
     | VernacSetOption _ | VernacUnsetOption _
     | VernacDeclareReduction _
-    | VernacExtend _ ) -> ()
+    | VernacExtend _ 
+    | VernacInductive _) -> ()
   | Some _, _ -> Errors.error "This command does not support Locality"
 
 (* Vernaculars that take a polymorphism flag *)
-- 
cgit v1.2.3