Move do_primitive from comassumption to its own module.

Primitives don't have anything to do with assumptions.

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;