Cleanup ComAssumption

The general idea is to move tests on scope=Discharge and on
Lib.sections_are_opened up in the call stack. This allows better
control over the universe manipulation.

There are some corner case behaviour change, eg:
- [Context (foo:=bla)] outside a section correctly declares an
  axiom (fix #10668)
- (not observable) universes for [Variable A B : Type] in section are declared only once
- universes and universe names for [Axiom A B : Type] are declared
  only once. This changes the qualification of the universe name:
  before it was the last axiom (so [B.u0]), now it's the first
  one ([A.u0]).
  Probably nobody cares about this.
- context outside section uses different [kind]

I'm not sure why context outside a section behaves differently based
on whether we're in a module type, I tried to preserve it but maybe we
should uniformize.

The universe manipulation for Axiom (in the declare_assumptions
function) is a bit awkward, maybe when there are multiple monomorphic
axioms instead of trying to attach the universes to the first one we
should just declare them separately like with Context. OTOH unlike
with context dropping the universe names seems incorrect.

1 files changed, 28 insertions, 9 deletions

diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index 44db47e1cc..ae9edefcac 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -23,27 +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
+
+(** 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."]