| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
Move to the right alphabetical ordering, fix dates, institutions.
Also add Jim, but not all the other missing people because I
officially renounce to keeping this file up-to-date.
|
|
Also remove Pierre Letouzey from the list because his contribution was
the numeral notation feature which ended up being backported to 8.9,
after the branching, but before the first beta release.
|
|
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.
|
|
This (partially) reverts commit 3984f3c1db51f7b788ad49eafb7647774e8d1f53.
This broke clients wanting to inspect the enviroment, see
https://github.com/coq/coq/pull/7745#issuecomment-411597610
There is a need for clients to inspect the global environment, we keep
the record private as to concerns regarding its use, so even if no
function in the kernel is taking a `globals` as an input, we transmit
to clients its read-only nature.
We take the opportunity to refactor the record into a module with
scoped constructors.
|
|
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.
|
|
sections
Reviewed-by: ppedrot
|
|
|
|
|
|
|
|
projections
Reviewed-by: fajb
|
|
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
Ack-by: vbgl
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: herbelin
Reviewed-by: ppedrot
|
|
- Specialised hash and equality functions.
Avoid collisions in extreme scenarios.
- Flags to disable the use of the caches.
fixes #10772
|
|
universe unification
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
|
|
We disallow adding univ constraints wich refer to polymorphic
universes, and monomorphic constants and inductives when polymorphic
universes or constraints are present.
Every other combination is already correctly discharged by the kernel.
|
|
|
|
Reviewed-by: maximedenes
|
|
Should be 1:1 equivalent to the previous code, this is semantics preserving
factorization.
|
|
|
|
|
