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.

0 files changed, 0 insertions, 0 deletions