| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
Instead of threading the universe state and making it grow, we make clear
in the signature that the differed side-effects generate constraints to be
added.
|
|
This reduces the attack surface of the API, as actually there is only a back
and forth between the two modules, and side-effects validity certificates are
intuitively nothing more than safe environments.
|
|
|
|
|
|
|
|
After some analysis this should be taken care of by
`Safe_typing.add_constant`
It was added in
https://github.com/coq/coq/commit/f7338257584ba69e7e815c7ef9ac0d24f0dec36c
, so maybe @gares can provide more context as to how is this stuff
supposed to work.
|
|
We provide a function `completion_candidates id` that will return a
list of candidates global references that have id as prefix.
This should be reasonably efficient, however UI still need to call
`shortest_qualid_of_global` which is a bit heavy. How to improve this
in the future is an open question.
cc: #7164
|
|
This is very useful to compute efficiently a list of prefixes. Will be
used in conjunction with the nametab to provide completion.
Example of use:
```
let cprefix x y = String.(compare x (sub y 0 (min (length x) (length y)))) in
M.filter_range (cprefix "foo") m
```
We could of course maintain a trie, but this is less invasive an
should work at our scale.
|
|
|
|
changes.
|
|
|
|
Since the removal of the dependency in camlp5 for CLexer, it looks like this
file was never generated, leading to installation failure. We add it as a
dependency of the install step.
|
|
We partially hand-translated so as to result in the minimal diff possible.
|
|
In favor of a constr_of_monomorphic_global function. When people
move to the new Coqlib interface they will also see this deprecation
message encouraging them to think about the best move.
This commit changes a few references to constr_of_global and replaces
them with a constr_of_monomorphic_global which makes it apparent that
this is not the function to call to globalize polymorphic references.
The remaining parts using constr_of_monomorphic_global are easily
identifiable using this: omega, btauto, ring, funind and auto_ind_decl
mainly (this fixes firstorder). What this means is that the symbols
registered for these tactics have to be monomorphic for now.
|
|
In general, `Nametab` is not a module you want to open globally as it
exposes very generic identifiers such as `push` or `global`.
Thus, we remove all global opens and qualify `Nametab` access. The
patch is small and confirms the hypothesis that `Nametab` access
happens in few places thus it doesn't need a global open.
It is also very convenient to be able to use `grep` to see accesses to
the namespace table.
|
|
|
|
This fixes the CI until this commit is merged into master.
|
|
|
|
|
|
|
|
|
|
|
|
We had a brief leftovers of the ocamlbuild experiment that are not
relevant anymore as it was removed from the tree a few years ago.
p.s: The amount of cruft we have in the `dev/build/windows` folder is
staggering, see for example what `git grep ocamlbuild` returns.
|
|
This file is already mostly in the required style so I wanted to see
what it looks like.
For a couple matches I locally disabled the warning as it was too
annoying otherwise (`when` clauses are especially annoying).
There are a couple places where I think it clearly looks better (eg
assoc_defined at the beginning of the file) but overall I'm not all
that convinced.
What do other people think?
|
|
|
|
|
|
I'd like to add this convention as it is very convenient for the
development of dev tools. Example, I can do `setup-coq-devs ltac
equations` and then get a fully composed tree. Similarly for preparing
overlays.
|
|
|
|
This allows to drop the ltac2 folder inside the Coq dir and have it
compose with the Coq build.
I've fixed build warnings by the way.
|
|
This is needed for compatibility with directory-listing
infrastructure.
|
|
|
|
|
|
|
|
Thus the adhoc univops can be removed at the end of the deprecation period.
Should we keep exposing restrict_universe_context or make people go
through restrict?
restrict_universe_context is used directly only by newring, where it's
a choice between
let univs = UState.restrict_universe_context univs vars in
and
let univs = UState.(context_set (restrict (of_context_set univs) vars)) in
|
|
It's basically an occur check so it makes sense to put it in vars
|
|
Such a basic function can live in Univ rather than the higher level UnivGen.
|
|
They are impractical since we need to get the level out to register it
afterwards.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
