From 5685e37442e49ce77831a371c471716c3ccb0a2b Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sun, 18 Aug 2019 21:18:18 +0200 Subject: Move do_primitive from comassumption to its own module. Primitives don't have anything to do with assumptions. --- vernac/comAssumption.ml | 27 --------------------------- vernac/comAssumption.mli | 2 -- vernac/comPrimitive.ml | 37 +++++++++++++++++++++++++++++++++++++ vernac/comPrimitive.mli | 11 +++++++++++ vernac/vernac.mllib | 1 + vernac/vernacentries.ml | 2 +- 6 files changed, 50 insertions(+), 30 deletions(-) create mode 100644 vernac/comPrimitive.ml create mode 100644 vernac/comPrimitive.mli diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index f6debd8777..a56cf9ab9a 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -190,33 +190,6 @@ let do_assumptions ~program_mode ~poly ~scope ~kind nl l = in () -let do_primitive id prim typopt = - if Lib.sections_are_opened () then - CErrors.user_err Pp.(str "Declaring a primitive is not allowed in sections."); - if Dumpglob.dump () then Dumpglob.dump_definition id false "ax"; - let env = Global.env () in - let evd = Evd.from_env env in - let evd, typopt = Option.fold_left_map - (interp_type_evars_impls ~impls:empty_internalization_env env) - evd typopt - in - let evd = Evd.minimize_universes evd in - let uvars, impls, typopt = match typopt with - | None -> Univ.LSet.empty, [], None - | Some (ty,impls) -> - EConstr.universes_of_constr evd ty, impls, Some (EConstr.to_constr evd ty) - in - let evd = Evd.restrict_universe_context evd uvars in - let uctx = UState.check_mono_univ_decl (Evd.evar_universe_context evd) UState.default_univ_decl in - let entry = { prim_entry_type = typopt; - prim_entry_univs = uctx; - prim_entry_content = prim; - } - in - let _kn : Names.Constant.t = - declare_constant ~name:id.CAst.v ~kind:Decls.IsPrimitive (PrimitiveEntry entry) in - Flags.if_verbose Feedback.msg_info Pp.(Id.print id.CAst.v ++ str " is declared") - let named_of_rel_context l = let open EConstr.Vars in let open RelDecl in diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index 2715bd8305..44db47e1cc 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -47,5 +47,3 @@ val context : poly:bool -> local_binder_expr list -> unit - -val do_primitive : lident -> CPrimitives.op_or_type -> constr_expr option -> unit diff --git a/vernac/comPrimitive.ml b/vernac/comPrimitive.ml new file mode 100644 index 0000000000..06fafddafb --- /dev/null +++ b/vernac/comPrimitive.ml @@ -0,0 +1,37 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* Univ.LSet.empty, [], None + | Some (ty,impls) -> + EConstr.universes_of_constr evd ty, impls, Some (EConstr.to_constr evd ty) + in + let evd = Evd.restrict_universe_context evd uvars in + let uctx = UState.check_mono_univ_decl (Evd.evar_universe_context evd) UState.default_univ_decl in + let entry = Entries.{ + prim_entry_type = typopt; + prim_entry_univs = uctx; + prim_entry_content = prim; + } + in + let _kn : Names.Constant.t = + Declare.declare_constant ~name:id.CAst.v ~kind:Decls.IsPrimitive (Declare.PrimitiveEntry entry) in + Flags.if_verbose Feedback.msg_info Pp.(Names.Id.print id.CAst.v ++ str " is declared") diff --git a/vernac/comPrimitive.mli b/vernac/comPrimitive.mli new file mode 100644 index 0000000000..c0db1cc464 --- /dev/null +++ b/vernac/comPrimitive.mli @@ -0,0 +1,11 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* CPrimitives.op_or_type -> Constrexpr.constr_expr option -> unit diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 4868182bb3..d9d993f5b5 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -26,6 +26,7 @@ Indschemes Obligations ComDefinition Classes +ComPrimitive ComAssumption ComInductive ComFixpoint diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index bc47ad8699..87abb9da59 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2607,7 +2607,7 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with | VernacPrimitive (id, prim, typopt) -> VtDefault(fun () -> unsupported_attributes atts; - ComAssumption.do_primitive id prim typopt) + ComPrimitive.do_primitive id prim typopt) | VernacComments l -> VtDefault(fun () -> unsupported_attributes atts; -- cgit v1.2.3