Merge PR #10670: ComAssumption cleanup

Ack-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot

14 files changed, 247 insertions, 205 deletions

diff --git a/kernel/section.mli b/kernel/section.mli
index fc3ac141e4..56b4d9ba8f 100644
--- a/kernel/section.mli
+++ b/kernel/section.mli
@@ -83,5 +83,3 @@ val replacement_context : Environ.env -> 'a t -> Opaqueproof.work_list
 (** Section segments of all declarations from this section. *)
 
 val is_in_section : Environ.env -> GlobRef.t -> 'a t -> bool
-
-val is_polymorphic_univ : Level.t -> 'a t -> bool
diff --git a/library/lib.ml b/library/lib.ml
index 991e23eb3a..0d9efe2d5d 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -425,9 +425,6 @@ let extract_worklist info =
 
 let sections () = Safe_typing.sections_of_safe_env @@ Global.safe_env ()
 
-let is_polymorphic_univ u =
-  Section.is_polymorphic_univ u (sections ())
-
 let replacement_context () =
   Section.replacement_context (Global.env ()) (sections ())
 
diff --git a/library/lib.mli b/library/lib.mli
index d3315b0f2e..59d77480e9 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -183,8 +183,6 @@ val is_in_section : GlobRef.t -> bool
 
 val replacement_context : unit -> Opaqueproof.work_list
 
-val is_polymorphic_univ : Univ.Level.t -> bool
-
 (** {6 Discharge: decrease the section level if in the current section } *)
 
 (* XXX Why can't we use the kernel functions ? *)
diff --git a/tactics/declare.ml b/tactics/declare.ml
index b24a97e2d4..3590146dfb 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -52,11 +52,7 @@ let name_instance inst =
 
 let declare_universe_context ~poly ctx =
   if poly then
-    (* FIXME: some upper layers declare universes several times, we hack around
-      by checking whether the universes already exist. *)
-    let (univs, cstr) = ctx in
-    let univs = Univ.LSet.filter (fun u -> not (Lib.is_polymorphic_univ u)) univs in
-    let uctx = Univ.ContextSet.to_context (univs, cstr) in
+    let uctx = Univ.ContextSet.to_context ctx in
     let nas = name_instance (Univ.UContext.instance uctx) in
     Global.push_section_context (nas, uctx)
   else
@@ -302,7 +298,7 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind
 (** Declaration of section variables and local definitions *)
 type variable_declaration =
   | SectionLocalDef of Evd.side_effects proof_entry
-  | SectionLocalAssum of { typ:Constr.types; univs:Univ.ContextSet.t; poly:bool; impl:Glob_term.binding_kind }
+  | SectionLocalAssum of { typ:Constr.types; impl:Glob_term.binding_kind; }
 
 (* This object is only for things which iterate over objects to find
    variables (only Prettyp.print_context AFAICT) *)
@@ -315,11 +311,10 @@ let declare_variable ~name ~kind d =
   if Decls.variable_exists name then
     raise (AlreadyDeclared (None, name));
 
-  let impl,opaque,poly = match d with (* Fails if not well-typed *)
-    | SectionLocalAssum {typ;univs;poly;impl} ->
-      let () = declare_universe_context ~poly univs in
+  let impl,opaque = match d with (* Fails if not well-typed *)
+    | SectionLocalAssum {typ;impl} ->
       let () = Global.push_named_assum (name,typ) in
-      impl, true, poly
+      impl, true
     | SectionLocalDef (de) ->
       (* The body should already have been forced upstream because it is a
          section-local definition, but it's not enforced by typing *)
@@ -342,8 +337,7 @@ let declare_variable ~name ~kind d =
         secdef_type = de.proof_entry_type;
       } in
       let () = Global.push_named_def (name, se) in
-      Glob_term.Explicit, de.proof_entry_opaque,
-      poly
+      Glob_term.Explicit, de.proof_entry_opaque
   in
   Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty name) (GlobRef.VarRef name);
   Decls.(add_variable_data name {opaque;kind});
@@ -608,28 +602,12 @@ let do_universe ~poly l =
 let do_constraint ~poly l =
   let open Univ in
   let u_of_id x =
-    let level = Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x in
-    Lib.is_polymorphic_univ level, level
-  in
-  let in_section = Lib.sections_are_opened () in
-  let () =
-    if poly && not in_section then
-      CErrors.user_err ~hdr:"Constraint"
-                    (str"Cannot declare polymorphic constraints outside sections")
-  in
-  let check_poly p p' =
-    if poly then ()
-    else if p || p' then
-      CErrors.user_err ~hdr:"Constraint"
-                    (str "Cannot declare a global constraint on " ++
-                    str "a polymorphic universe, use "
-                    ++ str "Polymorphic Constraint instead")
+    Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x
   in
   let constraints = List.fold_left (fun acc (l, d, r) ->
-     let p, lu = u_of_id l and p', ru = u_of_id r in
-     check_poly p p';
-     Constraint.add (lu, d, ru) acc)
-    Constraint.empty l
+      let lu = u_of_id l and ru = u_of_id r in
+      Constraint.add (lu, d, ru) acc)
+      Constraint.empty l
   in
   let uctx = ContextSet.add_constraints constraints ContextSet.empty in
   declare_universe_context ~poly uctx
diff --git a/tactics/declare.mli b/tactics/declare.mli
index da66a2713c..f4bfdb1547 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -36,7 +36,7 @@ type 'a proof_entry = {
 
 type variable_declaration =
   | SectionLocalDef of Evd.side_effects proof_entry
-  | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:Glob_term.binding_kind }
+  | SectionLocalAssum of { typ:types; impl:Glob_term.binding_kind; }
 
 type 'a constant_entry =
   | DefinitionEntry of 'a proof_entry
diff --git a/test-suite/bugs/closed/bug_10669.v b/test-suite/bugs/closed/bug_10669.v
new file mode 100644
index 0000000000..433e300acb
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10669.v
@@ -0,0 +1,12 @@
+
+Context (A0:Type) (B0:A0).
+Definition foo0 := B0.
+
+Set Universe Polymorphism.
+Context (A1:Type) (B1:A1).
+Definition foo1 := B1.
+
+Section S.
+  Context (A2:Type) (B2:A2).
+  Definition foo2 := B2.
+End S.
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index a89fd64999..d13ea707bb 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -157,12 +157,12 @@ Type@{UnivBinders.58} -> Type@{i}
 axbar is universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant UnivBinders.axbar
-axfoo' : Type@{axbar'.u0} -> Type@{axbar'.i}
+axfoo' : Type@{axfoo'.u0} -> Type@{axfoo'.i}
 
 axfoo' is not universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant UnivBinders.axfoo'
-axbar' : Type@{axbar'.u0} -> Type@{axbar'.i}
+axbar' : Type@{axfoo'.u0} -> Type@{axfoo'.i}
 
 axbar' is not universe polymorphic
 Argument scope is [type_scope]
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index e3f90ab98c..8cf5e3a8b4 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -11,7 +11,6 @@
 open CErrors
 open Util
 open Vars
-open Declare
 open Names
 open Context
 open Constrexpr_ops
@@ -41,27 +40,24 @@ let should_axiom_into_instance = let open Decls in function
     true
   | Definitional | Logical | Conjectural -> !axiom_into_instance
 
-let declare_assumption is_coe ~poly ~scope ~kind typ univs pl imps impl nl {CAst.v=name} =
-let open DeclareDef in
-match scope with
-| Discharge ->
-  let univs = match univs with
-    | Monomorphic_entry univs -> univs
-    | Polymorphic_entry (_, univs) -> Univ.ContextSet.of_context univs
-  in
+let declare_variable is_coe ~kind typ imps impl {CAst.v=name} =
   let kind = Decls.IsAssumption kind in
-  let decl = SectionLocalAssum {typ; univs; poly; impl} in
-  let () = declare_variable ~name ~kind decl in
-  let () = assumption_message name in
+  let decl = Declare.SectionLocalAssum {typ; impl} in
+  let () = Declare.declare_variable ~name ~kind decl in
+  let () = Declare.assumption_message name in
   let r = GlobRef.VarRef name in
   let () = maybe_declare_manual_implicits true r imps in
   let env = Global.env () in
   let sigma = Evd.from_env env in
   let () = Classes.declare_instance env sigma None true r in
   let () = if is_coe then Class.try_add_new_coercion r ~local:true ~poly:false in
-  (r,Univ.Instance.empty)
+  ()
 
-| Global local ->
+let instance_of_univ_entry = function
+  | Polymorphic_entry (_, univs) -> Univ.UContext.instance univs
+  | Monomorphic_entry _ -> Univ.Instance.empty
+
+let declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl {CAst.v=name} =
   let do_instance = should_axiom_into_instance kind in
   let inl = let open Declaremods in match nl with
     | NoInline -> None
@@ -70,42 +66,65 @@ match scope with
   in
   let kind = Decls.IsAssumption kind in
   let decl = Declare.ParameterEntry (None,(typ,univs),inl) in
-  let kn = declare_constant ~name ~local ~kind decl in
+  let kn = Declare.declare_constant ~name ~local ~kind decl in
   let gr = GlobRef.ConstRef kn in
   let () = maybe_declare_manual_implicits false gr imps in
   let () = Declare.declare_univ_binders gr pl in
-  let () = assumption_message name in
+  let () = Declare.assumption_message name in
   let env = Global.env () in
   let sigma = Evd.from_env env in
   let () = if do_instance then Classes.declare_instance env sigma None false gr in
-  let local = match local with ImportNeedQualified -> true | ImportDefaultBehavior -> false in
-  let () = if is_coe then Class.try_add_new_coercion gr ~local ~poly in
-  let inst = match univs with
-    | Polymorphic_entry (_, univs) -> Univ.UContext.instance univs
-    | Monomorphic_entry _ -> Univ.Instance.empty
+  let local = match local with
+    | Declare.ImportNeedQualified -> true
+    | Declare.ImportDefaultBehavior -> false
   in
+  let () = if is_coe then Class.try_add_new_coercion gr ~local ~poly in
+  let inst = instance_of_univ_entry univs in
   (gr,inst)
 
 let interp_assumption ~program_mode sigma env impls c =
   let sigma, (ty, impls) = interp_type_evars_impls ~program_mode env sigma ~impls c in
   sigma, (ty, impls)
 
-(* When monomorphic the universe constraints are declared with the first declaration only. *)
-let next_uctx =
-  let empty_uctx = Monomorphic_entry Univ.ContextSet.empty in
+(* When monomorphic the universe constraints and universe names are
+   declared with the first declaration only. *)
+let next_univs =
+  let empty_univs = Monomorphic_entry Univ.ContextSet.empty, UnivNames.empty_binders in
   function
-  | Polymorphic_entry _ as uctx -> uctx
-  | Monomorphic_entry _ -> empty_uctx
+  | Polymorphic_entry _, _ as univs -> univs
+  | Monomorphic_entry _, _ -> empty_univs
 
-let declare_assumptions idl is_coe ~scope ~poly ~kind typ uctx pl imps nl =
-  let refs, _ =
-    List.fold_left (fun (refs,uctx) id ->
-        let ref = declare_assumption is_coe ~scope ~poly ~kind typ uctx pl imps Glob_term.Explicit nl id in
-        ref::refs, next_uctx uctx)
-      ([],uctx) idl
-  in
-  List.rev refs
+let context_set_of_entry = function
+  | Polymorphic_entry (_,uctx) -> Univ.ContextSet.of_context uctx
+  | Monomorphic_entry uctx -> uctx
 
+let declare_assumptions ~poly ~scope ~kind univs nl l =
+  let open DeclareDef in
+  let () = match scope with
+    | Discharge ->
+      (* declare universes separately for variables *)
+      Declare.declare_universe_context ~poly (context_set_of_entry (fst univs))
+    | Global _ -> ()
+  in
+  let _, _ = List.fold_left (fun (subst,univs) ((is_coe,idl),typ,imps) ->
+      (* NB: here univs are ignored when scope=Discharge *)
+      let typ = replace_vars subst typ in
+      let univs,subst' =
+        List.fold_left_map (fun univs id ->
+            let refu = match scope with
+              | Discharge ->
+                declare_variable is_coe ~kind typ imps Glob_term.Explicit id;
+                GlobRef.VarRef id.CAst.v, Univ.Instance.empty
+              | Global local ->
+                declare_axiom is_coe ~local ~poly ~kind typ univs imps nl id
+            in
+            next_univs univs, (id.CAst.v, Constr.mkRef refu))
+          univs idl
+      in
+      subst'@subst, next_univs univs)
+      ([], univs) l
+  in
+  ()
 
 let maybe_error_many_udecls = function
   | ({CAst.loc;v=id}, Some _) ->
@@ -175,139 +194,112 @@ let do_assumptions ~program_mode ~poly ~scope ~kind nl l =
      IMO, thus I think we should adapt `prepare_parameter` to handle
      this case too. *)
   let sigma = Evd.restrict_universe_context sigma uvars in
-  let uctx = Evd.check_univ_decl ~poly sigma udecl in
+  let univs = Evd.check_univ_decl ~poly sigma udecl in
   let ubinders = Evd.universe_binders sigma in
-  let _, _ = List.fold_left (fun (subst,uctx) ((is_coe,idl),typ,imps) ->
-      let typ = replace_vars subst typ in
-      let refs = declare_assumptions idl is_coe ~poly ~scope ~kind typ uctx ubinders imps nl in
-      let subst' = List.map2
-          (fun {CAst.v=id} (c,u) -> (id, Constr.mkRef (c,u)))
-          idl refs
-      in
-      subst'@subst, next_uctx uctx)
-      ([], uctx) l
+  declare_assumptions ~poly ~scope ~kind (univs,ubinders) nl l
+
+let context_subst subst (name,b,t,impl) =
+  name, Option.map (Vars.substl subst) b, Vars.substl subst t, impl
+
+let context_insection sigma ~poly ctx =
+  let uctx = Evd.universe_context_set sigma in
+  let () = Declare.declare_universe_context ~poly uctx in
+  let fn subst (name,_,_,_ as d) =
+    let d = context_subst subst d in
+    let () = match d with
+      | name, None, t, impl ->
+        let kind = Decls.Context in
+        declare_variable false ~kind t [] impl (CAst.make name)
+      | name, Some b, t, impl ->
+        (* We need to get poly right for check_same_poly *)
+        let univs = if poly then Polymorphic_entry ([| |], Univ.UContext.empty)
+          else Monomorphic_entry Univ.ContextSet.empty
+        in
+        let entry = Declare.definition_entry ~univs ~types:t b in
+        let _ : GlobRef.t = DeclareDef.declare_definition ~name ~scope:DeclareDef.Discharge
+            ~kind:Decls.Definition UnivNames.empty_binders entry []
+        in
+        ()
+    in
+    Constr.mkVar name :: subst
   in
+  let _ : Vars.substl = List.fold_left fn [] ctx 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)
+let context_nosection sigma ~poly ctx =
+  let univs =
+    match ctx, poly with
+    | [_], _ | _, true -> Evd.univ_entry ~poly sigma
+    | _, false ->
+      (* Multiple monomorphic axioms: declare universes separately to
+         avoid redeclaring them. *)
+      let uctx = Evd.universe_context_set sigma in
+      let () = Declare.declare_universe_context ~poly uctx in
+      Monomorphic_entry Univ.ContextSet.empty
   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;
-              }
+  let fn subst d =
+    let (name,b,t,_impl) = context_subst subst d in
+    let kind = Decls.(IsAssumption Logical) in
+    let decl = match b with
+      | None ->
+        Declare.ParameterEntry (None,(t,univs),None)
+      | Some b ->
+        let entry = Declare.definition_entry ~univs ~types:t b in
+        Declare.DefinitionEntry entry
+    in
+    (* let local = Declare.ImportNeedQualified in *)
+    let cst = Declare.declare_constant ~name ~kind ~local:Declare.ImportNeedQualified decl in
+    let () = Declare.assumption_message name in
+    let env = Global.env () in
+    (* why local when is_modtype? *)
+    let () = if Lib.is_modtype() || Option.is_empty b then
+        Classes.declare_instance env sigma None (Lib.is_modtype()) (GlobRef.ConstRef cst)
+    in
+    Constr.mkConstU (cst,instance_of_univ_entry univs) :: subst
   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
-  let acc, ctx =
-    List.fold_right
-      (fun decl (subst, ctx) ->
-         let id = match get_name decl with Anonymous -> invalid_arg "named_of_rel_context" | Name id -> id in
-               let d = match decl with
-           | LocalAssum (_,t) -> id, None, substl subst t
-           | LocalDef (_,b,t) -> id, Some (substl subst b), substl subst t in
-               (EConstr.mkVar id :: subst, d :: ctx))
-      l ([], [])
-  in ctx
+  let _ : Vars.substl = List.fold_left fn [] ctx in
+  ()
 
 let context ~poly l =
   let env = Global.env() in
   let sigma = Evd.from_env env in
-  let sigma, (_, ((env', fullctx), impls)) = interp_context_evars ~program_mode:false env sigma l in
+  let sigma, (_, ((_env, ctx), impls)) = interp_context_evars ~program_mode:false env sigma l in
   (* Note, we must use the normalized evar from now on! *)
   let sigma = Evd.minimize_universes sigma in
   let ce t = Pretyping.check_evars env (Evd.from_env env) sigma t in
-  let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) fullctx in
-  let ctx =
-    try named_of_rel_context fullctx
-    with e when CErrors.noncritical e ->
-      user_err Pp.(str "Anonymous variables not allowed in contexts.")
-  in
-  let univs =
-    match ctx with
-    | [] -> assert false
-    | [_] -> Evd.univ_entry ~poly sigma
-    | _::_::_ ->
-      if Lib.sections_are_opened ()
-      then
-        (* More than 1 variable in a section: we can't associate
-           universes to any specific variable so we declare them
-           separately. *)
-        begin
-          let uctx = Evd.universe_context_set sigma in
-          Declare.declare_universe_context ~poly uctx;
-          if poly then Polymorphic_entry ([||], Univ.UContext.empty)
-          else Monomorphic_entry Univ.ContextSet.empty
-        end
-      else if poly then
-        (* Multiple polymorphic axioms: they are all polymorphic the same way. *)
-        Evd.univ_entry ~poly sigma
-      else
-        (* Multiple monomorphic axioms: declare universes separately
-           to avoid redeclaring them. *)
-        begin
-          let uctx = Evd.universe_context_set sigma in
-          Declare.declare_universe_context ~poly uctx;
-          Monomorphic_entry Univ.ContextSet.empty
-        end
-  in
-  let fn (name, b, t) =
-    let b, t = Option.map (EConstr.to_constr sigma) b, EConstr.to_constr sigma t in
-    if Lib.is_modtype () && not (Lib.sections_are_opened ()) then
-      (* Declare the universe context once *)
-      let kind = Decls.(IsAssumption Logical) in
-      let decl = match b with
-        | None ->
-          Declare.ParameterEntry (None,(t,univs),None)
-        | Some b ->
-          let entry = Declare.definition_entry ~univs ~types:t b in
-          Declare.DefinitionEntry entry
+  let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) ctx in
+  (* reorder, evar-normalize and add implicit status *)
+  let ctx = List.rev_map (fun d ->
+      let {binder_name=name}, b, t = RelDecl.to_tuple d in
+      let name = match name with
+        | Anonymous -> user_err Pp.(str "Anonymous variables not allowed in contexts.")
+        | Name id -> id
       in
-      let cst = Declare.declare_constant ~name ~kind decl in
-      let env = Global.env () in
-      Classes.declare_instance env sigma (Some Hints.empty_hint_info) true (GlobRef.ConstRef cst);
-      ()
-    else
+      let b = Option.map (EConstr.to_constr sigma) b in
+      let t = EConstr.to_constr sigma t in
       let test x = match x.CAst.v with
         | Some (Name id',_) -> Id.equal name id'
         | _ -> false
       in
-      let impl = if List.exists test impls then Glob_term.Implicit else Glob_term.Explicit in
-      let scope =
-        if Lib.sections_are_opened () then DeclareDef.Discharge else DeclareDef.Global ImportDefaultBehavior in
-      match b with
-      | None ->
-        let _, _ =
-          declare_assumption false ~scope ~poly ~kind:Decls.Context t
-            univs UnivNames.empty_binders [] impl
-            Declaremods.NoInline (CAst.make name)
-        in
-        ()
-      | Some b ->
-        let entry = Declare.definition_entry ~univs ~types:t b in
-        let _gr = DeclareDef.declare_definition
-            ~name ~scope:DeclareDef.Discharge
-            ~kind:Decls.Definition UnivNames.empty_binders entry [] in
-        ()
+      let impl = Glob_term.(if List.exists test impls then Implicit else Explicit) in
+      name,b,t,impl)
+      ctx
   in
-  List.iter fn (List.rev ctx)
+  if Lib.sections_are_opened ()
+  then context_insection sigma ~poly ctx
+  else context_nosection sigma ~poly ctx
+
+(* Deprecated *)
+let declare_assumption is_coe ~poly ~scope ~kind typ univs pl imps impl nl name =
+let open DeclareDef in
+match scope with
+| Discharge ->
+  let univs = match univs with
+    | Monomorphic_entry univs -> univs
+    | Polymorphic_entry (_, univs) -> Univ.ContextSet.of_context univs
+  in
+  let () = Declare.declare_universe_context ~poly univs in
+  declare_variable is_coe ~kind typ imps impl name;
+  GlobRef.VarRef name.CAst.v, Univ.Instance.empty
+| Global local ->
+  declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl name
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index 2715bd8305..ae9edefcac 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -23,29 +23,46 @@ val do_assumptions
   -> (ident_decl list * constr_expr) with_coercion list
   -> unit
 
-(** returns [false] if the assumption is neither local to a section,
-    nor in a module type and meant to be instantiated. *)
-val declare_assumption
+val declare_variable
   : coercion_flag
-  -> poly:bool
-  -> scope:DeclareDef.locality
   -> kind:Decls.assumption_object_kind
   -> Constr.types
-  -> Entries.universes_entry
-  -> UnivNames.universe_binders
   -> Impargs.manual_implicits
   -> Glob_term.binding_kind
+  -> variable CAst.t
+  -> unit
+
+val declare_axiom
+  : coercion_flag
+  -> poly:bool
+  -> local:Declare.import_status
+  -> kind:Decls.assumption_object_kind
+  -> Constr.types
+  -> Entries.universes_entry * UnivNames.universe_binders
+  -> Impargs.manual_implicits
   -> Declaremods.inline
   -> variable CAst.t
   -> GlobRef.t * Univ.Instance.t
 
 (** Context command *)
 
-(** returns [false] if, for lack of section, it declares an assumption
-    (unless in a module type). *)
 val context
   :  poly:bool
   -> local_binder_expr list
   -> unit
 
-val do_primitive : lident -> CPrimitives.op_or_type -> constr_expr option -> unit
+(** Deprecated *)
+val declare_assumption
+  : coercion_flag
+  -> poly:bool
+  -> scope:DeclareDef.locality
+  -> kind:Decls.assumption_object_kind
+  -> Constr.types
+  -> Entries.universes_entry
+  -> UnivNames.universe_binders
+  -> Impargs.manual_implicits
+  -> Glob_term.binding_kind
+  -> Declaremods.inline
+  -> variable CAst.t
+  -> GlobRef.t * Univ.Instance.t
+[@@ocaml.deprecated "Use declare_variable or declare_axiom instead."]
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/lemmas.ml b/vernac/lemmas.ml
index c7a588d2b4..e49277c51b 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -265,7 +265,8 @@ let save_remaining_recthms env sigma ~poly ~scope ~udecl uctx body opaq i { Rect
            Univ.ContextSet.of_context univs
          | Monomorphic_entry univs -> univs
        in
-       let c = Declare.SectionLocalAssum {typ=t_i; univs; poly; impl} in
+       let () = Declare.declare_universe_context ~poly univs in
+       let c = Declare.SectionLocalAssum {typ=t_i; impl} in
        let () = Declare.declare_variable ~name ~kind c in
        GlobRef.VarRef name, impargs
      | Global local ->
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 03bf008529..afc701edbc 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 40786fe0b4..4734ce1fb9 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2476,7 +2476,7 @@ let 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;