diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/classes.ml | 36 | ||||
| -rw-r--r-- | vernac/comAssumption.mli | 2 | ||||
| -rw-r--r-- | vernac/comDefinition.mli | 4 | ||||
| -rw-r--r-- | vernac/comFixpoint.ml | 1 | ||||
| -rw-r--r-- | vernac/comFixpoint.mli | 2 | ||||
| -rw-r--r-- | vernac/comInductive.ml | 2 | ||||
| -rw-r--r-- | vernac/comInductive.mli | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 7 |
8 files changed, 37 insertions, 19 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 25d893bfb..192cc8a55 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -374,16 +374,34 @@ let context poly l = with e when CErrors.noncritical e -> user_err Pp.(str "Anonymous variables not allowed in contexts.") in - let uctx = ref (Evd.universe_context_set sigma) in + let univs = + let uctx = Evd.universe_context_set sigma in + match ctx with + | [] -> assert false + | [_] -> + if poly + then Polymorphic_const_entry (Univ.ContextSet.to_context uctx) + else Monomorphic_const_entry uctx + | _::_::_ -> + if Lib.sections_are_opened () + then + begin + Declare.declare_universe_context poly uctx; + if poly then Polymorphic_const_entry Univ.UContext.empty + else Monomorphic_const_entry Univ.ContextSet.empty + end + else if poly + then Polymorphic_const_entry (Univ.ContextSet.to_context uctx) + else + begin + Declare.declare_universe_context poly uctx; + Monomorphic_const_entry Univ.ContextSet.empty + end + in let fn status (id, b, t) = let b, t = Option.map (to_constr sigma) b, to_constr sigma t in if Lib.is_modtype () && not (Lib.sections_are_opened ()) then (* Declare the universe context once *) - let univs = if poly - then Polymorphic_const_entry (Univ.ContextSet.to_context !uctx) - else Monomorphic_const_entry !uctx - in - let () = uctx := Univ.ContextSet.empty in let decl = match b with | None -> (ParameterEntry (None,(t,univs),None), IsAssumption Logical) @@ -405,10 +423,6 @@ let context poly l = in let impl = List.exists test impls in let decl = (Discharge, poly, Definitional) in - let univs = if poly - then Polymorphic_const_entry (Univ.ContextSet.to_context !uctx) - else Monomorphic_const_entry !uctx - in let nstatus = match b with | None -> pi3 (ComAssumption.declare_assumption false decl (t, univs) Universes.empty_binders [] impl @@ -422,6 +436,4 @@ let context poly l = in status && nstatus in - if Lib.sections_are_opened () then - Declare.declare_universe_context poly !uctx; List.fold_left fn true (List.rev ctx) diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index f235de350..56e324376 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -19,7 +19,7 @@ open Decl_kinds (** {6 Parameters/Assumptions} *) val do_assumptions : locality * polymorphic * assumption_object_kind -> - Vernacexpr.inline -> (Vernacexpr.ident_decl list * constr_expr) with_coercion list -> bool + Vernacexpr.inline -> (ident_decl list * constr_expr) with_coercion list -> bool (************************************************************************) (** Internal API *) diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index 0d6367291..6f81c4575 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -17,7 +17,7 @@ open Constrexpr (** {6 Definitions/Let} *) val do_definition : program_mode:bool -> - Id.t -> definition_kind -> Vernacexpr.universe_decl_expr option -> + Id.t -> definition_kind -> universe_decl_expr option -> local_binder_expr list -> red_expr option -> constr_expr -> constr_expr option -> unit Lemmas.declaration_hook -> unit @@ -27,6 +27,6 @@ val do_definition : program_mode:bool -> (** Not used anywhere. *) val interp_definition : - Vernacexpr.universe_decl_expr option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr -> + universe_decl_expr option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr -> constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * Univdecls.universe_decl * Impargs.manual_implicits diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index edfe7aa81..a794c2db0 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -14,7 +14,6 @@ open Pretyping open Evarutil open Evarconv open Misctypes -open Vernacexpr module RelDecl = Context.Rel.Declaration diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index b181984e0..36c2993af 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -32,7 +32,7 @@ val do_cofixpoint : type structured_fixpoint_expr = { fix_name : Id.t; - fix_univs : Vernacexpr.universe_decl_expr option; + fix_univs : Constrexpr.universe_decl_expr option; fix_annot : Misctypes.lident option; fix_binders : local_binder_expr list; fix_body : constr_expr option; diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 457a1da05..c59286d1a 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -57,7 +57,7 @@ let push_types env idl tl = type structured_one_inductive_expr = { ind_name : Id.t; - ind_univs : Vernacexpr.universe_decl_expr option; + ind_univs : universe_decl_expr option; ind_arity : constr_expr; ind_lc : (Id.t * constr_expr) list } diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index b8d85c8d9..833935724 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -47,7 +47,7 @@ val declare_mutual_inductive_with_eliminations : type structured_one_inductive_expr = { ind_name : Id.t; - ind_univs : Vernacexpr.universe_decl_expr option; + ind_univs : universe_decl_expr option; ind_arity : constr_expr; ind_lc : (Id.t * constr_expr) list } diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 0ff6d9c17..5779c07ab 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -805,7 +805,14 @@ let vernac_end_segment ({v=id} as lid) = (* Libraries *) +let warn_require_in_section = + let name = "require-in-section" in + let category = "deprecated" in + CWarnings.create ~name ~category + (fun () -> strbrk "Use of “Require” inside a section is deprecated.") + let vernac_require from import qidl = + if Lib.sections_are_opened () then warn_require_in_section (); let qidl = List.map qualid_of_reference qidl in let root = match from with | None -> None |