| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Reviewed-by: ejgallego
Ack-by: SkySkimmer
Ack-by: gares
Ack-by: ppedrot
|
|
|
|
AFAIK `Fail Instance` cannot open a goal.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
proofs.
We forbid commands that may open proofs inside proofs.
|
|
|
|
Since some state handling refactoring, `purify_stm` was no longer
protecting against assignement of cur_id, resulting in confusing
behavior w.r.t. cache.
|
|
|
|
(fix #9204)
|
|
|
|
workers
|
|
- deprecate the old 5-tuple accessor in favor of a view record,
- move `name` and `kind` proof data from `Proof_global` to `Proof`,
this will prove useful in subsequent functionalizations of the
interface, in particular this is what abstract, which lives in the
monads, needs in order no to access global state.
- Note that `Proof.t` and `Proof_global.t` are redundant anyways.
|
|
The error-resiliency feature may have managed to reach the end
of the document by recovering some error
|
|
|
|
|
|
|
|
comments.
|
|
This is a pre-requisite to use automated formatting tools such as
`ocamlformat`, also, there were quite a few places where the comments
had basically no effect, thus it was confusing for the developer.
p.s: Reading some comments was a lot of fun :)
|
|
Rename Univ.Level.{Qualid -> UGlobal}, remove Univ.Level.Id.
Remove the ability to split the argument of `Univ.Level.Level` into a
dirpath*int pair (except by going through string hacks like
detyping/pretyping(/funind) does).
Id.of_string_soft to turn unnamed universes into qualid is pushed up
to detyping. (TODO some followup PR clean up more)
This makes it pointless to have an opaque type for ints in
Univ.Level: it would only be used as argument to
Univ.Level.UGlobal.make, ie
~~~
open Univ.Level
let x = UGlobal.make dp (Id.make n)
(* vs *)
let x = UGlobal.make dp n
~~~
Remaining places which create levels from ints are various hacks (eg
the dummy in inductive.ml, the Type.n universes in ugraph
sort_universes) and univgen.
UnivGen does have an opaque type for ints used as univ ids since they
get manipulated by the stm.
NB: build breaks due to ocamldep issue if UGlobal is named Global instead.
|
|
Remote counters were trying to build universe levels (as opposed to
simple integers), but did not have access to the right dirpath at
construction time. We fix it by constructing the level only at use time,
and we introduce some abstractions for qualified and unqualified level
names.
|
|
We make `declaration_hook`s optional arguments everywhere, and thus we
avoid some "fake" functions having to be passed.
This identifies positively the code really using hooks [funind,
rewrite, coercions, program, and canonicals] and helps moving toward
some hope of reification.
|
|
This makes setting the option outside of the synchronized summary impossible.
|
|
|
|
write_function
|
|
Before this patch, it had no effect.
|
|
The semantics of this flag was not clear, it had several rather
orthogonal effects. Also, it should probably have been another value of
`-async-proofs-mode`, rather than a separate flag, as its combination
with e.g. `-async-proofs-mode off` is unclear.
|
|
|
|
|
|
|
|
We group the extension API and datatypes under `Vernacextend`.
This means that the base plugin dependency is now `coq.vernac` from
`coq.stm`.
This is quite important as for example the LSP server won't like to
link the STM in.
LTAC still depends on the STM by means of the ltac_profile part tho.
The next step could be to move the extension point below `Vernacexpr`.
|
|
|
|
Fix #8989.
This adds an option -topfile taking a path so that inferring the right
dirpath is done by the toplevel after processing -Q/-R instead of the
client having to do it.
|
|
This PR fixes an issues that was bugging me for some time, namely that
`Vernacinterp` really means `Vernacextend`.
We thus rename the file and move the associated functions there, which
were incorrectly placed in `Vernacentries`.
Note the beneficial effects on reducing the `.mli` API.
|
|
|
|
|
|
|
|
|
|
Commands need to request the attributes they use, with the API
encouraging them to error on unsupported attributes.
|
|
|
|
|
|
|
|
Lintian found some spelling errors in the Debian packaging for coq. Fix
them most places they appear in the current source. (Don't change
documentation anchor names, as that would invalidate external
deeplinks.)
This also fixes a bug in coqdoc: prior to this commit, coqdoc would
highlight `instanciate` but not `instantiate`.
|
|
|
|
After the introduction of `EConstr`, "normalization" has become
unnecessary, we thus deprecate the `nf_*` family of functions.
Test-suite and CI pass after the fix for #8513.
|
