| Age | Commit message (Collapse) | Author |
|---|
|
We remove calls of `Lemmas.Info.make` that where using the default
parameters, as this is mostly dead code now.
This brings into question quite a few things, in particular, the
uneven support of `scope` attributes by different commands / plugins.
We don't attempt to solve that yet, hopefully the ongoing constant
saving path refactoring will be able to take care of these
inconsistencies.
|
|
Instead of doing (simplified code)
~~~ocaml
let check env kn cb =
let flags = env.flags in
let env' = set_flags env cb.flags in
...
let env = add_constant cb kn (if poly then env else env') in
set_flags env flags
~~~
(NB: when not poly env' has only the typing flags different from env)
we do
~~~ocaml
let check env kn cb =
let env = set_flags env cb.flags in
...
()
let check env kn cb =
let () = check env kn cb in
add_constant cb kn env
~~~
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
|
|
Now everything that does not have any dependencies goes to the first stage.
The rest goes to the first stage following all its dependencies.
All jobs specifying a dependencies keyword also specify a needs keyword.
|
|
Reviewed-by: Zimmi48
|
|
|
|
Master version of the fix for #10679
|
|
|
|
We go back to the kind of workflow we had in CircleCI thanks to GitLab
12.2 new needs keyword.
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: vbgl
|
|
Reviewed-by: mattam82
|
|
We use the `(coq.pp ...)` dune directive which will produce correct
error messages for `.mlg` files.
Unfortunately we cannot yet use the automatic opam generation features
of Dune 1.10, as this does require a fully native Dune build.
Dune 1.6-1.10 has quite a few other improvements that could be used by
Coq, for example for promote modes.
I have fixed a couple of documentation issues. `Drop` and `ocamldebug`
have been tested in this version.
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
TLC and CPDT are not actually tested. No point in keeping them as if they were.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
|
|
|
|
Reviewed-by: ejgallego
|
|
deployed versions.
Reviewed-by: ejgallego
|
|
|
|
We move `binder_kind` to the pretyping AST, removing the last data
type in the now orphaned file `Decl_kinds`.
This seems a better fit, as this data is not relevant to the lower
layers but only used in `Impargs`.
We also move state keeping to `Impargs`, so now implicit declaration
must include the type. We also remove a duplicated function.
|
|
|
|
We update the URLs to the new ones, even if the previous continue to work.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
|
|
|
|
This file is unrelated to library, but to pretyping/unification.
This commit, along with others already submitted go towards the goal
of `library` containing only the handling of library objects.
|
|
This source of slowness has been observed in VST, but it is probably
pervasive. Most of the unification problems are not mentioning evars,
it is thus useless to compute the set of frozen evars upfront.
We also seize the opportunity to reverse the flag, because it is always
used negatively.
|
|
Reviewed-by: cpitclaudel
|
|
|
|
Now all relevant typing_flags are taken in account by the checker.
The different forms of assumptions are now printed by the checker.
|
|
type-in-type universes
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(co)fixpoints) and [check_positive] (for (co)inductive types).
|
|
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
|
|
* filter_app (moved from MSets/MSetRBT.v)
* filter_map
* filter_ext_in
* ext_in_filter
* filter_ext_in_iff
* filter_ext
* concat_filter_map
* combine_nil
* combine_firstn_l
* combine_firstn_r
* combine_firstn
* nodup_fixed_point
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
This should fix some bugs w.r.t. management of state introduced in
|
|
Fixes #10452
|
|
We place control attributes on their own, datatype, similarly to
regular attributes.
This is a step towards fixing #10452 , as we can now decouple control
attributes from the vernac AST itself, allowing to pass them
independently.
|
|
Reviewed-by: ppedrot
|
|
`Mlutil.simpl` and `Mlutil.atomic_eta_red` did some unsound eta-reductions as
follows:
(fun x0 ... xn => MLexn x0 ... xn) ->eta MLexn.
`MLexn` raises an exception thus is not a value in OCaml. So the above
simplification may change the behavior of extracted programs. This patch
restricts `atomic_eta_red` to eta-redexes whose core is both atomic and value.
Acknowledgement: This work is financially supported by Peano System Inc.
on-behalf-of: @peano-system <info@peano-system.jp>
|
|
false).
|
