| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
Reviewed-by: gares
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
(fix #10864)
Reviewed-by: SkySkimmer
|
|
|
|
|
|
demote_seff_univs
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot
|
|
Reviewed-by: gares
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: hendriktews
Reviewed-by: herbelin
Ack-by: mattam82
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
|
|
Reviewed-by: JasonGross
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
Reviewed-by: SkySkimmer
|
|
It's only called with extend:false from inside UState so we don't need
to expose it.
Not having to look at the whole `merge` function will hopefully help
those trying to understand side effects.
|
|
We don't need to call `UState.demote_seff_univs` as
`emit_side_effects` (`tclEFFECTS`) can do it for us.
|
|
Reviewed-by: Zimmi48
|
|
timeout keyword.
Reviewed-by: ejgallego
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
They probably don't need to be executable
|
|
Explain into the release process how to prepare the release notes.
|
|
|
|
|
|
Ack-by: ejgallego
Reviewed-by: vbgl
|
|
This allows UI clients to implement a different state management
strategy with regards to proofs, and in particular to override
`Vernacinterp.interp`.
This is work in progress towards having a true `VtTactic` which shall
not perform any state changes non-functionally, and actually removing
the series of `assert false` due to meta-vernacs.
|
|
Reviewed-by: cpitclaudel
|
|
Reviewed-by: vbgl
|
|
|
|
|
|
|
|
reduce or not.
Reviewed-by: jfehrle
|
|
There were 2:
- when declaring a constraint to avoid monomorphic constraint
referring to polymorphic univs, this check is redundant with the
check in Section.ml
- when declaring a universe context to avoid redeclaring universes,
this is not necessary after recent commits.
|
|
|
|
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.
|
|
Primitives don't have anything to do with assumptions.
|
|
(letins still declare universes in declare_variable as they use
entries)
The section check_same_poly is moved to declare_universe_context (it
makes more sense there, universe polymorphism doesn't apply to the
variables/letins themselves)
|
|
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
|
|
|
|
database
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
We only do it for entries and not declarations because the upper layers
rely on the kernel being able to quickly tell that a definition is improperly
used inside a section. Typically, tactics can mess with the named context
and thus make the use of section definitions illegal. This cannot happen in
the kernel but we cannot remove it due to the code dependency.
Probably fixing a soundness bug reachable via ML code only. We were doing
fancy things w.r.t. computation of the transitive closure of the the variables,
in particular lack of proper sanitization of the kernel input.
|
