Fix bugs 4389, 4390 and 4391 due to wrong handling of universe names

structure.

3 files changed, 23 insertions, 11 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 7c86d2d059..3995c4b1bc 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -38,8 +38,8 @@ open Indschemes
 open Misctypes
 open Vernacexpr
 
-let do_universe l = Declare.do_universe l  
-let do_constraint l = Declare.do_constraint l
+let do_universe poly l = Declare.do_universe poly l
+let do_constraint poly l = Declare.do_constraint poly l
 
 let rec under_binders env sigma f n c =
   if Int.equal n 0 then snd (f env sigma c) else
diff --git a/toplevel/command.mli b/toplevel/command.mli
index b1e1d7d060..b400f0fde2 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -20,8 +20,9 @@ open Pfedit
 (** This file is about the interpretation of raw commands into typed
     ones and top-level declaration of the main Gallina objects *)
 
-val do_universe : Id.t Loc.located list -> unit
-val do_constraint : (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit
+val do_universe : polymorphic -> Id.t Loc.located list -> unit
+val do_constraint : polymorphic ->
+  (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit
 
 (** {6 Hooks for Pcoq} *)
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index d04d6c9eda..2879947a91 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -552,12 +552,12 @@ let vernac_inductive poly lo finite indl =
       Errors.error "The Variant keyword cannot be used to define a record type. Use Record instead."
   | [ ( id , bl , c , b, RecordDecl (oc,fs) ), [] ] ->
       vernac_record (match b with Class true -> Class false | _ -> b)
-	poly finite id bl c oc fs
+       poly finite id bl c oc fs
   | [ ( id , bl , c , Class true, Constructors [l]), _ ] ->
       let f =
 	let (coe, ((loc, id), ce)) = l in
 	let coe' = if coe then Some true else None in
-	  (((coe', AssumExpr ((loc, Name id), ce)), None), [])
+  	  (((coe', AssumExpr ((loc, Name id), ce)), None), [])
       in vernac_record (Class true) poly finite id bl c None [f]
   | [ ( id , bl , c , Class true, _), _ ] ->
       Errors.error "Definitional classes must have a single method"
@@ -602,8 +602,19 @@ let vernac_combined_scheme lid l =
      List.iter (fun lid -> dump_global (Misctypes.AN (Ident lid))) l);
  Indschemes.do_combined_scheme lid l
 
-let vernac_universe l = do_universe l
-let vernac_constraint l = do_constraint l
+let vernac_universe loc poly l =
+  if poly && not (Lib.sections_are_opened ()) then
+    user_err_loc (loc, "vernac_universe",
+		  str"Polymorphic universes can only be declared inside sections, " ++
+		  str "use Monomorphic Universe instead");
+  do_universe poly l
+
+let vernac_constraint loc poly l =
+  if poly && not (Lib.sections_are_opened ()) then
+    user_err_loc (loc, "vernac_constraint",
+		  str"Polymorphic universe constraints can only be declared"
+		  ++ str " inside sections, use Monomorphic Constraint instead");
+  do_constraint poly l
 
 (**********************)
 (* Modules            *)
@@ -1870,8 +1881,8 @@ let interp ?proof ~loc locality poly c =
   | VernacCoFixpoint (local, l) -> vernac_cofixpoint locality poly local l
   | VernacScheme l -> vernac_scheme l
   | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l
-  | VernacUniverse l -> vernac_universe l
-  | VernacConstraint l -> vernac_constraint l
+  | VernacUniverse l -> vernac_universe loc poly l
+  | VernacConstraint l -> vernac_constraint loc poly l
 
   (* Modules *)
   | VernacDeclareModule (export,lid,bl,mtyo) ->
@@ -2034,7 +2045,7 @@ let check_vernac_supports_polymorphism c p =
     | VernacCoercion _ | VernacIdentityCoercion _
     | VernacInstance _ | VernacDeclareInstances _
     | VernacHints _ | VernacContext _
-    | VernacExtend _ ) -> ()
+    | VernacExtend _ | VernacUniverse _ | VernacConstraint _) -> ()
   | Some _, _ -> Errors.error "This command does not support Polymorphism"
 
 let enforce_polymorphism = function