diff options
| -rw-r--r-- | vernac/comAssumption.ml | 27 | ||||
| -rw-r--r-- | vernac/comAssumption.mli | 2 | ||||
| -rw-r--r-- | vernac/comPrimitive.ml | 37 | ||||
| -rw-r--r-- | vernac/comPrimitive.mli | 11 | ||||
| -rw-r--r-- | vernac/vernac.mllib | 1 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
6 files changed, 50 insertions, 30 deletions
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 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +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 + Constrintern.(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 = 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 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +val do_primitive : Names.lident -> 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; |