diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 25 |
1 files changed, 18 insertions, 7 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index d04d6c9ed..2879947a9 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 |